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 TPTP World
- Writing TPTP Problems
- Playing in the TPTP World.
- The ATP Process
  Get practice with
  - The Exercises in 1st order logic
  - The Exercises in typed 1st order logic
  - The Examples and a Challenge for the ATP Process
- Reality of ATP in the TPTP World
The Principles Behind the Practice
- Logical Consequence
- Logical Consequence by Truth Tables