The TPTP World Tutorial

Introduction

• A Motivating Example
• ATP, What is it?
• ATP, What is it Good For?
• 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?