Thomas Hillenbrand

Research Teaching Software

Automated Deduction for Equational Logic

Summer 2003

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.

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.

Examinations and Grading:

• An intermediate written examination is scheduled for Wednesday, June 11, in place of the tutorial.
• A final one will follow when the lecture is finished.
• For the final grade, the intermediate and the final one will be averaged in relation 1:3. For passing, this final grade must be better than 4.1.

Exercise Sheets: