Main lecture: Wed 8:30 to 10:00 in S3 057, weekly.
Exercises: to be announced
Overview
The purpose of this course is to give an overview on various aspects of equational reasoning, including unification, paramodulation, rewriting-based deduction and completion.
Implement the unification algorithm presented in the class in your favorite programming language. Deadline: January 10. Submit the code by email.
Literature
Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, United Kingdom, 1998.
Franz Baader and Jörg Siekmann. Unification Theory. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, pages 41-125. Oxford University Press, Oxford, UK, 1994.
Franz Baader and Wayne Snyder. Unification Theory. In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, pages 447-533. Elsevier Science Publishers, 2001.
Robert Nieuwenhuis and Albert Rubio. Paramodulation-Based Theorem Proving. In: Alan Robinson and Andrei Voronkov, editors. Handbook of Automated Reasoning. Volume 1, pp. 371-443, 2001.
Leo Bachmair and Harald Ganzinger, Equational Reasoning in Saturation-Based Theorem Proving, Chapter 11 of vol. I of Automated Deduction - A Basis for Applications, W. Bibel and P. Schmitt, eds., pp. 353-397, Kluwer, 1998.