Automated Theorem Proving: Course Content

White Board
Introduction
- What is ATP? (Lecture 24-08-20)
- Logical Consequence (Lecture 24-08-22)
- The TPTP World (Lecture 24-08-27)
  - ATP in your Web Browser
- Propositional Logic I (Lecture 24-08-22)
  - The Language
  - Logical Consequence by Truth Tables
  Now go play in the TPTP World (Lecture 24-08-27)
- 1st Order Logic I - The Language
  Now go play in the TPTP World (Lecture 24-08-29)
- Typed 1st Order Logic I - The Language
  Now go play in the TPTP World (Lecture 24-09-03)
- Some Stronger Logics in the TPTP World (Lecture 24-09-05)
Using ATP Systems in the TPTP World
- Writing TPTP Problems (for more details, see the TPTP Quick Guide)
- Examples in various logics (Lecture 24-08-27) (Lecture 24-08-29) (Lecture 24-09-03)
- The ATP Process (Lecture 24-09-03)
- You can get practice with
  - The Exercises in 1st order logic
  - The Exercises in typed 1st order logic
  - The Examples and Challenge for the ATP Process
Propositional logic II
- Clause Normal Form (Lecture 24-09-05)
- The DPLL and CDCL Algorithms (Lecture 24-09-10)
1st order logic II
General Purpose Improvements
- Heuristics (Lecture 24-09-24)
- Restrictions (Lecture 24-09-24) (Lecture 24-09-26)
Prolog
Refinements of the Resolution Procedure - Saturation Based
Equality Reasoning
- Paramodulation (Lecture 24-11-05)
  (Paramodulation (sucks) example)
- Superposition (Lecture 24-11-05) (Lecture 24-11-12)
  (Superposition example) (Superposition challenge answer) ( Superposition pure equality challenge answer)
Return to the Theory
- Overview (The theory stack)
- Conversion to CNF is equisatisfiable (i.e., an SPT) (Skolemization forward example)
- A set of clauses has a model iff it has a Herbrand model
- Resolution is a Herbrand SPT
- A Herbrand unsatisfiable set of clauses has a failure tree
- A fair resolution procedure is refutation complete
Refinements of the Resolution Procedure - Goal Oriented
Instantiation Based Methods
- The Gilmore Procedure