Lecture "Automated Reasoning", SS12 - Literature

Reformatted slides

• Lecture 01, 04/16/2012: [script]; [slides]
• Lecture 02, 04/19/2012: [script]; [slides]
• Lecture 03, 04/23/2012: [script]; [slides]
• Lecture 04, 04/26/2012: [script]; [slides]
• Lecture 05, 04/30/2012: [script]; [slides]
• Lecture 06, 05/03/2012: [script]; [slides]
• Lecture 07, 05/07/2012: [script]; [slides]
• Lecture 08, 05/10/2012: [script]; [slides]
• Lecture 09, 05/14/2012: [script]; [slides]
• Lecture 10, 05/21/2012: [script]; [slides]
• Lecture 11, 05/24/2012: [script]; [slides]
• Lecture 12, 05/31/2012: [script]; [slides]
• Lecture 13, 06/04/2012: [script]; [slides]
• Lecture 14, 06/11/2012: [script14-1]; [script14-2]; [slides14-1]; [slides14-2]; [slides14-3]
• Lecture 15, 06/14/2012: [script]; [slides]
• Lecture 16, 06/18/2012: [script]; [slides]
• Lecture 17, 06/21/2012: [script]; [slides]
• Lecture 18, 06/25/2012: See Lecture 17
• Lecture 19, 06/28/2012: [script]; [slides]
• Lecture 20, 07/02/2012: [script]; [slides]
• Lecture 21, 07/05/2012: [script]; [slides]
• Lecture 22, 07/09/2012: [slides]
• Lecture 23, 07/12/2012: [script]; [slides]
• Lecture 24, 07/16/2012: [script]; [slides]
• Lecture 25, 07/19/2012: [script]; [slides]
• Lecture 26, 07/23/2012: [slides]



• Complete Script (up to last lecture): [script]; [slides]

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