The TPTP World Tutorial

Introduction

• Automated Reasoning, What is it?
• Automated Reasoning, What is it Good For?
• Automated Reasoning, What Systems are Successful?
• The TPTP World
  • The TPTP Language
  • ATP in your Web Browser
  • A TPTP Example

Examples for the Education Process

• Propositional Logic
• First-order Logic
• Typed First-order Logic
• Typed First-order Logic with Arithmetic
• 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?