Theorem Proving and Equality

Technische Universität Dresden Institut für Theoretische Informatik Lehrstuhl für Automatentheorie

Dr. Barbara Morawska

Course Description

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.

Organization

The lecture takes place in room E005, the tutorials usually take place in the computer lab E046.

• 4.04, DS 3 - lecture (E005);
• 13.04, DS 5 - lecture (E005);
• 18.04, DS 3 - tutorial (E005);
• 20.04, DS 5 - lecture (E005);
• 27.04, DS 5 - lecture (E005);
• 2. 05, DS 3 - lecture (E005);
• 4.05, DS 5 - tutorial (lab E046);
• 11.05, DS 5 - lecture (E005);
• 16.05, DS 3 - lecture (E005);
• 18.05, DS 5 - tutorial (lab E046);
• 25.05, DS 5 - lecture (E005);
• 6.06, DS 3 - lecture (E005);
• 8.06, DS 5 - tutorial (lab E046);
• 15.06, DS 5 - lecture (E005);
• 20.06, DS 3 - lecture (E005);
• 22.06, DS 5 - tutorial (lab E046); -> this tutorial is moved to 27.06, DS 3 (E005)
• 29.06, DS 5 - lecture (E005);
• 4.07, DS 3 - lecture (E005);
• 6.07, DS 5 - tutorial (lab E046);
• 13.07, DS 5 - lecture (E005);

DS 3 = 11.10 - 12.40, DS 5 = 14.50 - 16.20.

Course Material

Some slides used in the lecture will be available here.

• example for otter
• the same example using sos
• the same example using paramodulation
• the first example for SPASS
• paramodulation in SPASS
• reduction -- definitions
• reductions -- properties
• orders -- properties
• more definitions
• facts -- proofs left as homework
• refutation soundness and completeness
• deletion rules
• Inference System G
• Model generation
• Inference system H

Exercises:

• Exercises 1
• Exercises 2
• Exercises 3
• Exercises 4
  examples for OTTER
  examples for SPASS
• Exercises 5
• Exercises 6

Credits / Examinations

Computational logic students can earn 4 credits by attending this lecture. The lecture can be used in the module TCSL and IT. In order to get the credits, CL students have to actively participate in the classes and pass an oral examination at the end of the term.

References

• 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.
• William McCune. Otter 3.3 Reference Manual, August 2003.
• 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.
• F. Baader, T. Nipkow. Term Rewriting and All That. ISBN 0-521-77920-0, Cambridge University Press, 1998.
• 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).