Automated Theorem Proving: The TPTP World
Introduction
The TPTP Problem Library
The TSTP Solution Library
The TPTP Language
Introduction
TPTP Format for Problems
TPTP Format for Derivations
TPTP Format for Finite Interpretations
The Syntax BNF
The SZS Ontology
Introduction
Full Details
SZS Standards for Answers
(forthcoming)
The TPTP and TSTP Libraries
www.tptp.org
TPTP History
TPTP Organization
TPTP Problems
Documentation
TSTP Organization
TSTP Solutions
Problem and System Ratings
The Higher-order TPTP
Introduction
The THF Language
The THF TPTP
THF Tools
TPTP Tools and Systems
TPTP2T - Problem and Solution Selector
TPTP2X and TPTP4X - Problem and Solution Manipulation
SystemOnTPTP - ATP Systems and Tools
GDV - Semantic Derivation Verification
SSCPA - Competitive Parallelism
Prophet - Prophesying Axiom Relevance
SRASS - Semantic Selection of Axioms
AGInT - Generating Interesting Theorems
IDV - Interactive Viewing of Derivations
System??T?TP - Doing it all Online
Why Does it Work?