The TPTP World Tutorial
Introduction
ATP, What is it?
ATP, What is it Good For?
The TPTP World
A TPTP Example
Examples for the Education Process
Propositional Logic
First-order Logic
Typed First-order Logic
Typed eXtended First-order Logic
Typed Higher-order Logic
Non-classical Typed Logic
The ATP Process
The ATP Process
Examples for Practice
A Theorem with Nice Axioms
A Theorem with Contradictory Axioms
A Theorem with Nasty Axioms
A Non-Theorem with Nice Axioms
A Challenge Theorem
The End - Any Questions?