Lecture "Automated Reasoning" - Literature

Reformatted slides

• Lecture 1, 04/17/2008: [pdf] [ps]
• Lecture 2, 04/13/2008: [pdf] [ps]
• Lecture 3, 04/24/2008: [pdf] [ps]
• Lecture 4, 04/29/2008: [pdf] [ps]
• Lecture 5, 05/06/2008: [pdf] [ps]
• Lecture 6, 05/08/2008: [pdf] [ps]
• Lecture 7, 05/13/2008: [pdf] [ps]
• Lecture 8, 05/15/2008: [pdf] [ps]
• Lecture 9, 05/20/2008: [pdf] [ps]
• Lecture 10, 05/27/2008: [pdf] [ps]
• Lecture 11, 05/29/2008: [pdf] [ps]
• Lecture 12, 06/03/2008: [pdf] [ps]
• Lecture 13, 06/03/2008: [pdf] [ps], --> DHCP Example: [dhcp.pdf], [dhcp.dfg]
• Lecture 14, 06/10/2008: [pdf] [ps]
• Lecture 15, 06/12/2008: [pdf] [ps]
• Lecture 16, 06/17/2008: [pdf] [ps]
• Lecture 17, 06/19/2008: [pdf] [ps]
• Lecture 18, 06/24/2008: [pdf] [ps]
• Lecture 19, 06/26/2008: [pdf] [ps]
• Lecture 20, 07/01/2008: [pdf] [ps]
• Lecture 21, 07/03/2008: [pdf] [ps]
• Lecture 22, 07/08/2008: [pdf] [ps]
• Lecture 23, 07/10/2008: [pdf] [ps]
• Lecture 24-26: [pdf] [ps]
• Complete Script: [pdf] [ps]

Slides of talk from first lecture

• Slides [ppt]

Dictionary

• English-German dictionary of deduction-related terms: [pdf] [ps]

Course material from other lectures

• Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann:
  Slides for "Automated Reasoning" SS 2004.
  Online at http://www.mpi-inf.mpg.de/~uwe/lehre/autreas/readings.html.
• Gert Smolka:
  Lecture notes for "Einführung in die Computationale Logik" SS 2003.
  Online at http://www.ps.uni-sb.de/courses/cl-ss03/skript/.

Propositional logic, first-order logic, tableaux calculi

• Melvin Fitting:
  First-Order Logic and Automated Theorem Proving.
  Springer-Verlag, New York, 1996.
• Uwe Schöning:
  Logik für Informatiker.
  Spektrum Akademischer Verlag, 2000

Termination, well-founded orderings, confluence, unification

• Franz Baader and Tobias Nipkow:
  Term Rewriting and All That.
  Cambridge Univ. Press, 1998.

Further readings

• Leo Bachmair and Harald Ganzinger
  Resolution Theorem Proving, in "Handbook of Automated Reasoning", pages 19-99.
  Elsevier, 2001.
• Robert Nieuwenhuis and Albert Rubio
  Paramodulation-Based Theorem Proving, in "Handbook of Automated Reasoning", pages 371-443.
  Elsevier, 2001.
• Andreas Nonnengart and Christoph Weidenbach
  Computing small clause normal forms, in "Handbook of Automated Reasoning", pages 335-367.
  Elsevier, 2001.
• Christoph Weidenbach
  Combining Superposition, Sorts and Splitting, in "Handbook of Automated Reasoning", pages 1965-2012.
  Elsevier, 2001.

• Automated Reasoning:
• Lecturers
• Start
• When and Where
• Prerequisites
• Exercises
• Literature
• Registration
• Certificate
• Grading
• Previous AR Lectures