ON THIS PAGE:

Course Objectives

Prerequisites

Approach

Typical Text

Course Objectives
Introduce research in automatic theorem proving.

Prerequisites
Prerequisite, COMP 825.

Approach
We will cover methods of theorem proving that can be programmed on a computer. That is, the computer is given a list of axioms and a desired conclusion or theorem, and attempts to find a proof of the theorem from the axioms. Such theorem proving programs have applications in program verification, proof checking, and artificial intelligence. A good theorem prover can also be a useful instructional aid when used as a proof checker. We will have a couple of theorem provers available for students to use. The course content is flexible and will be partly determined by the interests of the students who enroll.

There are a number of fairly general theorem proving methods, as well as some that are more specialized and only deal with assertions of certain specialized forms. We will discuss methods of theorem proving for the propositional calculus, natural deduction and resolution based methods for the first order predicate calculus, specialized methods based on term rewriting systems for theorems involving equality, and specialized methods for Presburger arithmetic and other such theories.

The course will also touch on a number of areas of my own research, such as extensions of Prolog to full first order logic, the use of theorem provers to solve logic puzzles and constraint satisfaction problems, specialized methods for near propositional calculus and set theory, term rewriting systems, the use of abstraction or analogy in theorem proving, and applications of theorem provers to expert systems. I will probably lecture largely independent of the text but will refer to it as necessary.

There will probably be five or six homeworks, a mid semester exam, and a project. The project may be a programming project, an attempt to prove a number of theorems on the various provers, or a research project. The grade will be approximately 20% homework, 30% mid semester exam, and 50% project. The mid semester exam will tentatively be near the middle of March during class period.

Typical Text
The text will be Fitting, First-Order Logic and Automated Theorem Proving. Other useful books are Bundy, The Computer Modelling of Mathematical Reasoning, Chang and Lee, Symbolic Logic and Mechanical Theorem Proving, Manna, Mathematical Theory of Computation, and Loveland, Automated Theorem Proving.