The TPTP World Tutorial
Introduction
ATP, What is it?
A Motivating Example
ATP, What is it Good For?
The TPTP World
Another Motivating 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 Process Flowchart
Examples for Practice
(click)
A Theorem with Nice Axioms
A Non-Theorem with Nice Axioms
A Theorem with Nasty Axioms
A Challenge Theorem
The End - Any Questions?