TPTP, TSTP, CASC, etc.
Automated Reasoning in Practice

Introduction

• ATP, What is it?
• ATP, What is it Good For?
• ATP, What Systems are Successful?
• TPTP Infrastructure

TPTP, TSTP, CASC

• The TPTP Problem Library
• The TPTP Language
• The SZS Ontology
• The TSTP Solution Library
• Problem and System Ratings
• The CADE ATP System Competition

The Higher-order TPTP

• Introduction
• The THF Language
• The THF TPTP
• THF Tools

Tools and Systems

• TPTP2T - Problem and Solution Selector
• TPTP2X and TPTP4X - Problem and Solution Manipulation
• SystemOnTPTP - ATP Systems and Tools
• SSCPA - Competitive Parallelism
• Prophet - Prophesying Axiom Relevance by Symbol Overlap
• APRILS - Prophesying Axiom Relevance by LSA
• SRASS - Semantic Selection of Axioms
• MANSEX - Multiple Answer Extraction
• SPASS-XDB - External Data Access for ATP
• GDV - Semantic Derivation Verification
• AGInT - Generating Interesting Theorems
• IDV - Interactive Viewing of Derivations
• System??T?TP - ATP in your Web Browser

Applications

• Certifiable program sythesis at NASA
• Cross-verification of the Mizar Mathematical Library
• Knowledge-based Reasoning in SUMO and Cyc
• Pervasive formal verification in Verisoft
• Controlled Natural Language Proving

• Future Acronyms
• Why Does it Work?