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.
Lecturer:
Uwe Waldmann <uwe@mpi-inf.mpg.de>
Tutor:
Thomas Hillenbrand <hillen@mpi-inf.mpg.de>
Summary of the lecture evaluation
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.
Tutorial [Thomas Hillenbrand]
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)
Examination sheets:
Intermediate exam
[English/PDF]
[English/PS]
[German/PDF]
[German/PS]
Final exam
[English/PDF]
[English/PS]
[German/PDF]
[German/PS]
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.
Previous |
Up |
Next
Uwe Waldmann
<
uwe@mpi-inf.mpg.de>,
2004-09-08.
Imprint |
Data Protection