QED and the TPTP World

Introduction

• What is the "TPTP World"?
• QED and the TPTP World

TPTP World Logics and Systems

• The TPTP Problem Library
• The TPTP Language (with Arithmetic)
• ATP Systems (with Arithmetic)
• The TSTP Solution Library (with SZS Ontology)

TPTP World Mathematics

• In the TPTP Problem Library
• The Mizar Mathematical Library
• The Naproche Project
• The Sledgehammer in Isabelle

TPTP World Services

• GDV - Semantic Derivation Verification
• AGInT - Automatic Generation of Interesting Theorems
• IDV - Interactive Derivation Viewing
• SystemOnTPTP - ATP in your Web Browser

Conclusion