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
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
Slides-I (Lectures I-VI),
Slides-II
(Lectures VII-X)
Student contributions:
Eyad Alkassar,
Joerg-Mueller,
Ruzica-Piskac-I,
Ruzica-Piskac-II,
Mohammed-Abushammala,
Andrey Shadrin,
Anna Marchenkova,
Marc Wagner,
Matthias
Berg,
Robert Grabowski
Assessment
Oral exam at the end of
term; here is the
schedule.
Theorem Provers
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)
Other useful reading:
- 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.