Automated Reasoning – Suggested Readings

Slides

Most recent version of these lecture notes: Course material Winter 2017/2018.

Current slides:
Lecture 20.04.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
Lecture 22.04.2004: no slides (see Huth/Ryan, Ch. 6.1/6.2 on OBDDs)
Lecture 27.04.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
Lecture 29.04.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
Lecture 04.05.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
Lecture 06.05.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
Lecture 11.05.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
Lecture 13.05.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
Lecture 18.05.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
Lecture 25.05.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
Lecture 27.05.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
Lecture 01.06.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
Lecture 03.06.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
Lecture 15.06.2004: no new slides
Lecture 17.06.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
Lecture 22.06.2004: no new slides
Lecture 24.06.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
Lecture 29.06.2004: no new slides
Lecture 01.07.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
Lecture 06.07.2004: no new slides
Lecture 12.07.2004: no new slides
Lecture 13.07.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]
    (Model construction theorem [PDF] [PS])
Lecture 15.07.2004: no new slides
Lecture 20.07.2004: no new slides
Lecture 22.07.2004 [PDF] [PS] [PS (4 per sheet)] [PS (8 per sheet)]

Harald Ganzinger:
Slides for the lecture "Logic for Computer Science" SS 2002.
Online at http://www.mpi-inf.mpg.de/~hg/Vorlesungen/Logik-SS02/.
(Only Slides1.* is relevant for the current lecture.)

Uwe Waldmann:
Slides for the lecture "Automated Deduction for Equational Logic" SS 2003.
Online at http://resources.mpi-inf.mpg.de/departments/rg1/teaching/eqlogic-ss03/.

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.

Michael Huth and Mark Ryan:
Logic in Computer Science: Modelling and Reasoning about Systems.
Cambridge Univ. Press, 2000.

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.


Previous | Up | Next
Uwe Waldmann <uwe@mpi-inf.mpg.de>, 2004-10-20.
Imprint | Data Protection