Lecture: Automated Theorem Proving
Contents
- Propositional Calculus: syntax, semantics, satisfiability, validity, clause normal form, resolution calculus, model construction, optimiesations
- First-Order Logic: syntax, semantics, Skolemisation, Herbrand models, unification, resolution calculus, well-founded orderings, refutational completeness
- Theorem Proving with Equality: term replacement systems, Church-Rosser theorem, Knuth-Bendix completion, paramodulation calculus, superpositions calculus
- Application Flow of Saturation Procedures: given clause algorithm, completeness and fairness
- Decidable fragments of First-Order Logic: Bernays-Schönfinkel class, monadic fragment, two-variable fragment, guarded fragment, resolution-based decision procedures
- Other Theorem Proving Methods: chaining calculus, disconnection calculus, instantiation calculus
Lecturer
Schedule
- Lectures
Tuesday: 12:30 — 14:00 in O27/121
Friday: 10:15 — 11:45 in O27/121
Consultation Hours: after the lectures or by appointment- Exercises
The exercises take place within the lecture time slots about every two weeks. The exact dates are announced in the lecture.
Vorlesungsunterlagen
The lecture notes, slides, and exercises are available through Moodle. The lecture notes can be printed through the Script printing system of SGI.
Literature and References
General reading material for the lecture:
- John Alan Robinson, Andrei Voronkov (Eds.). Handbook of Automated Reasoning, Elsevier and MIT Press 2001, ISBN 0-444-50813-9,0-262-18223-8: Volume 1, Chapter 2, Chapter 6, Chapter 7
- Uwe Schöning. Logik für Informatiker. Spektrum. ISBN 3-8274-1005-3
- Melvin Fitting. First-Order Logic and Automated Theorem Proving. Springer. ISBN 0-387-94593-8
- Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge Univ. Press, 1998, ISBN 978-0521779203
Technical Information
| Type: | Lecture for Master Students (3V / 1Ü) |
| Credit Points: | 6 |
| Curriculae: | Theoretische und Mathematische Methoden der Informatik (Kernfach/Kernmodul) Theoretische Informatik (Vertiefungsmodul) Intelligente Systeme (Vertiefungsmodul) |
| Related Lectures: | Intelligente Handlungsplanung Grundlagen des Semantic Web Multiagentensysteme |