## Theorem Proving with Equality |
Technische Universität Dresden |

The aim of this lecture is to review the fundamental techniques in the automated theorem proving in the first order logic with equality predicate. We will study completeness of various inference systems starting with Resolution, Ordered Resolution, Paramodulation and Superposition, i.e. saturation-based theorem provers. The main method of proving completeness, which we will use and study, is model generation and reduction of minimal counterexamples.

Prerequisites: an acquaintance with the basics of propositional and first-order logic is expected. We will also refer to the notions from the Term Rewriting Systems.

The lectures take place in room E005 every Friday, 14:50 - 16:20.

Computational logic students can earn 5 credits by attending this lecture.
The lecture can be used
in the module TCSL and PI.

In order to get the credits, CL students have to submit the assignments
and pass an oral
examination at the end of the term.

- L. Bachmair, H. Ganzinger. Resolution Theorem Proving,
Chap. 2 in
*Handbook of Automated Reasoning*, ed. A. Robinson, A. Voronkov, vol.1, North Holland 2001. - R. Nieuwenhuis, A. Rubio.
Paramodulation-Based Theorem Proving.
Chapter of
*Handbook of Automated Reasoning*ed. A. Robinson, A. Voronkov. ISBN 0-444-82949-0. Elsevier Science and MIT Press, North Holland 2001. - L. Bachmair, H. Ganzinger, Ch. Lynch, W. Snyder.
Basic Paramodulation. in
*Information and Computation*, vol. 121, nr.2, 1995, pp. 172-192. - Ch. Weidenbach. SPASS: Combining Superposition, Sorts and Splitting
Chapter of
*Handbook of Automated Reasoning*ed. A. Robinson, A. Voronkov. ISBN 0-444-82949-0. Elsevier Science and MIT Press, North Holland 2001. - L. Bachmair, N. Dershowitz, D.A.Plaisted. Completion without Failure.
Chap. 1 in
*Resolution of Equations in Algebraic Structures 2: Rewriting Techniques*, H. Ait-Kaci and M. Nivat, eds. pp. 1-30, Academic Press, New York (1989).

Barbara Morawska