Research Group 1: Automation of Logic
max planck institut
informatik
Lecture "Automated Reasoning", SS12 - Literature
Reformatted 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.
A
utomated Reasoning:
Le
c
turers
S
tart
W
hen and Where
P
rerequisites
E
xercises
Literat
u
re
Reg
i
stration
Certi
f
icate
G
rading
Previ
o
us AR Lectures