Automated Theorem Proving: Course Content

White Board
Introduction
- What is ATP?
- The TPTP World
TPTP World Logics
- Propositional Logic I - The Language
  Play in the TPTP World
- 1st Order Logic - The Language
  Play in the TPTP World
- Typed 1st Order Logic - The Language
  Play in the TPTP World
- Typed 1st Order Logic with Arithmetic - The Language
  Play in the TPTP World
- Some Stronger Logics, by examples
  Play in the TPTP World
A Naval Challenge
Using ATP Systems in the Real World
- Writing TPTP Problems
- A Why and How of Proof Verification
- The ATP Process
- Reality of ATP in the TPTP World
- Get practice with
  - The Exercises in 1st order logic
  - The Exercises in typed 1st order logic
  - The Challenges for the ATP Process
The Principles Behind the Practice
- Logical Consequence
- Logical Consequence by Truth Tables