Automated Theorem Proving in First-Order and Higher-Order Logic

Dates
Thursday, 16:15 -17:45, Room: HS 002, Bldg.: 45

Classification:
Special  Course, Logic and Computation, 6 Credit Points

Background Needed:
Basic knowledge about first-order logic and resolution based theorem proving is useful.
For some introductory reading see below (e.g. Huth, Fitting).

Lecturer

Christoph Benzmueller, Room 2.12, Tel. 4574,  Email: chris@ags.uni-sb.de

Preliminary Module Outline

The following module outline is preliminary and may be changed: Due to the overlap with the two related modules mentioned above the idea is to concentrate more on semantics and mechanisation of higher-order logic. This means that we will probably skip Lectures 1-5 and instead more deeply concentrate on the topics of Lectures 6-12.

Lecture 1-4 : Theorem Proving in Classical Propositional and First-Order Logic
• History
• Syntax and semantics of propositional and first-order logic
• Resolution for Propositional and first-order logic
• Completeness of first-order resolution via abstract consistency
Lecture 5: First-Order Theorem Provers in Practice
• Playing with some first-order theorem provers
• The TPTP library and format
• The comfortable use of theorem provers via the MathWeb software bus
Lecture 6-8: Introduction to Classical Higher-Order Logic
• Motivation and history
• Lambda calculus
• Syntax and semantics of higher-order logic
• Higher-order unification
Lecture 9+10: Theorem Proving in Higher-order Logic
• Resolution
• Primitive substitution
• Extensionality
• Defined and primitive equality
Lecture 11: Landscape of Higher-Order Semantics

Lecture 12: Higher-Order Theorem Provers in Practice

Assignments

They are included in the slides below. Here are the solutions (version from 22.July after lecture).

Slides

Assessment

Oral exam at the end of term;  here is the schedule.

Theorem Provers

OTTER
SPASS
HOL
TPS

A bunch of other provers can be found at http://www.mathweb.org/mathweb/services.html

Literature

Introduction to first-order logic and deduction systems:
• M. Fitting: First-Order Logic and Automated Theorem Proving. Springer. 1996 (2nd edition).
Introduction to higher-order logic:
• P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. 2002. Kluwer.
Introduction to typed lambda-calculus:
• H. Barendregt. Lambda Calculi with Types.  Handbook of  Logik  in  Computer  Science.  Oxford  University  Press. 1992. Eds. Samsom Abramsky, Dov Gabbay, Tom Maibaum.
At the core of the lecture:
• C. Benzmüller, C. Brown, and M. Kohlhase: Higher Order Semantics and Extensionality. Journal of Symbolic Logic. To appear. (74 pages). JSTOR. (pdf)
• C. Benzmüller: Comparing Approaches to Resolution based Higher-Order Theorem Proving. Synthese, (2002) 133(1-2):203-235. Kluwer. (pdf)
• M. Huth, M. Ryan. Logic in Computer Science. Modelling and reasoning about systems. 2000. Cambridge University Press.
• K.H. Blaesius, H.-J. Buerckert. Deduktionssysteme. Oldenbourg. 1992.
• A. Bundy. Survey of Automated Deduction. Informatics Research Report. Division of Informatics, University of Edinburgh. 1999.
• A. Church. A Formulation of Simple Theory of Types. Journal of Symbolic Logic. 1940. 5(2). pp 56-68.
• L. Henkin. Completeness in the Theory of Types. Journal of Symbolic Logic. 1950. 15(2). pp. 81-91.
• H. Barendregt, H. Geuvers. Proof-Assistants Using Dependent Type Systems. Handbook of Automated Reasoning , Vol. 2. Elsevier Science. 2001. pp. 1151-1234.
• G. Dowek. Higher-Order Unification and Matching. Handbook of Automated Reasoning, Vol. 2. Elsevier Science. 2001. pp. 1011-1060.
• P. B. Andrews. Classical Type Theory. Handbook of Automated Reasoning , Vol. 2. Elsevier Science. 2001. pp. 967-1004.
• W. Snyder, J. Gallier. Higher-Order Unification Revisited: Complete Sets of Transformations. Unification. Academic Press. 1990. pp. 565-604.
• H.P. Barendregt. Lambda Calculi with Types. Handbook of Logic in Computer Science.
• S. Thompson. Type Theory and Functional Programming. 1991. Addison-Wesley.
• M. Kohlhase. Beweissysteme mit Logiken hoeherer Stufe. Deduktion . Oldenbourg. 1992.
• Gerard P. Huet. A Mechanisation of Type Theory. Proceedings of the 3rd Joint Conference on Artificial Intelligence. 1973. pp. 139-146.
• Further literature will be mentioned in the lecture.