Management and Analysis of ATP System Proofs

Introduction

• ATP, What is it?
• ATP, What is it Good For?
• ATP, What Systems are Successful?
• The TPTP World
  • The TPTP Problem Library
  • The TSTP Solution Library
  • The SZS Ontology

Tools and Systems

• Selecting Problems and Solutions
• IDV - Interactive Viewing of Derivations
• Semantic Derivation Verification
• Rating Interesting Theorems
• Problem and System Ratings
• SSCPA - Competitive Parallelism

A Mathematical Application

• The Mizar Mathematical Library
• Cross-verification of the MML

Conclusion

• Why Does it Work?