From the TPTP to the TSTP

Introduction

• What is ATP?

The TPTP and Related Activities

• Thousands of Problems for Theorem Provers
  • Aims and Motivations
  • Inside the TPTP
  • SystemOnTPTP
• Revealing the PPPs and SPCs
• Problem and System Evaluation
• The CADE ATP System Competition

Meta-ATP Systems

• SSCPA
• CSSCPA
• RedAx and YiBS

The TSTP and Related Activities

• Thousands of Solutions from Theorem Provers
  • Aims and Motivations
  • Inside the TSTP
• Semantic Proof Verification
• Automatic Theorem Discovery

Conclusion