Lecture "Automated Reasoning", SS10 - Literature

Reformatted slides

• Lecture 1, 04/15/2010: [pdf]
• Lecture 2, 04/20/2010: [pdf]
• Lecture 3, 04/22/2010: [pdf]
• Lecture 4, 04/27/2010: [pdf]
• Lecture 5, 04/29/2010: [pdf]
• Lecture 6, 05/04/2010: [pdf]
• Lecture 7, 05/06/2010: [pdf]
• Lecture 8, 05/11/2010: [pdf]
• Lecture 9, 05/18/2010: [pdf]
• Lecture 10, 05/20/2010: [pdf]
• Lecture 11, 05/25/2010: [pdf]
• Lecture 12, 05/27/2010: [pdf]
• Lecture 13, 06/01/2010: [pdf]
• Lecture 14, 06/08/2010: [pdf]
• Lecture 15, 06/10/2010: [pdf]
• Lecture 16, 06/15/2010: Guest Lecture by Deepak Kapur:
  Kapur, D., 1997, Shostak's Congruence Closure as Completion, Rewriting Techniques and Applications, 8th International Conference, RTA-97, LNCS 1232, pp. 23-37.
• Lecture 17, 06/17/2010: [pdf]
• Lecture 18, 06/22/2010: [pdf]
• Lecture 19, 06/24/2010: [pdf]
• Lecture 20, 06/29/2010: [pdf]
• Lecture 21, 07/01/2010: [pdf]
• Lecture 22, 07/06/2010: [pdf]
• Lecture 23, 07/08/2010: [pdf]
• Lecture 24, 07/13/2010: [pdf]
• Lecture 25, 07/15/2010: Repetition
• Lecture 26, 07/20/2010: [pdf]
• Lecture 27, 07/22/2010: [pdf]



• Complete Script: [pdf]

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
• Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh (Editors)
  Handbook of Satisfiability
  IOS Press, 2009

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