Uwe Waldmann - Automated Deduction for Equational Logic

Lecture "Automated Deduction for Equational Logic" (SS 2003)

Time and Venue:
Lecture: Mondays, 14:15--16:00, Bldg 45, Room 001.
Tutorial: Wednesdays, 9:15--11:00, Bldg 46.1 (MPI), Room 022.

Topics:

Syntax and semantics of first-order logic,
Reduction systems and term rewriting (termination, confluence, critical pairs, etc.),
Termination orderings (e.g., path orderings, polynomial orderings, Knuth-Bendix ordering),
(Theory) unification,
Superposition calculus,
Theory reasoning (e.g., calculi with built-in asssociative and commutative operators, transitive relations, Abelian groups),
Implementation issues.

Slides:
Lecture 28.04.2003 [PDF] [PS]
Lecture 05.05.2003 [PDF] [PS]
Lecture 12.05.2003 [PDF] [PS]
Lecture 19.05.2003 [PDF] [PS]
Lecture 26.05.2003 [PDF] [PS]
Lecture 02.06.2003 [PDF] [PS]
Lecture 16.06.2003 [PDF] [PS]
Lecture 23.06.2003 [PDF] [PS]
Lecture 30.06.2003 [PDF] [PS]
Lecture 07.07.2003 [PDF] [PS] (Model construction theorem [PDF] [PS])
Lecture 14.07.2003 [PDF] [PS]
Lecture 21.07.2003 [PDF] [PS] (Thomas Hillenbrand)

References:

Franz Baader and Tobias Nipkow, Term Rewriting and All That, Cambridge Univ. Press, 1998.
Harald Ganzinger, Logic for Computer Science, Lecture Slides, 2002, online at http:/~hg/Vorlesungen/Logik-SS02/.
Leo Bachmair and Harald Ganzinger, Rewrite-based equational theorem proving with selection and simplification, Journal of Logic and Computation, 4(3):217-247, 1994.
Leo Bachmair and Harald Ganzinger, Equational reasoning in saturation-based theorem proving, in Wolfgang Bibel and Peter H. Schmitt, eds., Automated Deduction - A Basis for Applications, Vol. I: Foundations - Calculi and Methods, ch. 11, pp. 353-397, Kluwer Academic Publishers, 1998.
Robert Nieuwenhuis and Albert Rubio, Paramodulation-based theorem proving. in John Alan Robinson and Andrei Voronkov, eds., Handbook of Automated Reasoning, Vol. I, ch. 7, pp. 371-443, Elsevier Science, 2001.