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?