System??T?TP - ATP in your Web Browser

SystemOnTPTP

• A suite of ATP systems
• SSCPA - Competitive Parallelism
• System recommendations (as used by SSCPA)
• System Rating reports
• Available online at www.tptp.org/cgi-bin/SystemOnTPTP

SystemB4TPTP

• Problem syntax conversion
• Parsers and pretty printing (BNF-based and tptp2X and tptp4X)
• FOF-CNF conversion (E and FLOTTER)
• Type checking (syntactic and Twelf-based)
• Axiom relevance measures (APRILS and Prophet)
• Available online at www.tptp.org/cgi-bin/SystemB4TPTP

SystemOnTSTP

• Solution syntax conversion
• Parsers and pretty printing (BNF-based and tptp4X)
• GDV - Semantic Derivation Verification
• AGInT - Interestingness Rating
• Answer extraction and proof summarization
• IDV - Interactive Viewing of Derivations
• Available online at www.tptp.org/cgi-bin/SystemOnTSTP