System on TMTP

This interface is for processing models. If you want to solve problems, use the SystemOnTPTP interface. If you want to process solutions more generally, use the SystemOnTSTP interface.

The TPTP Needs Money   See the TPTP web page for details, benefits, and process of making a donation.

Model

 TMTP Model (e.g., KRS176+1.005-FMo)
Browse TMTP
Formulae to interpret
 TMTP Formulae (Model example)
 Local file to upload
 URL to fetch from

Output mode
 Result
 Progress
 System
 Everything
Extras (Nothing else)
 SOnTMTP
Our server does not output results until all tasks are completed. Be patient while the systems do their thing. Results are presented using the SZS problem status ontology.
System CPU s Transform Format Command Application
 BNFParser 0.0  s Checks syntax according to BNF, for TH0 TF1 TF0 FOF CNF
 BNFParserDrill 0.0  s Checks syntax according to BNF, producing user interface, for TH0 TF1 TF0 FOF CNF
 BNFParserTree 0.0  s Checks syntax according to BNF, producing parse tree, for TH0 TF1 TF0 FOF CNF
 GMV 0.0  s Verifies model against formulae, between SZS lines (ask Geoff)
 InterpretByATP 0.0  s Evaluates formulae against a model, between SZS lines (ask Geoff)
 TPTP2JSON 0.1  s Converts to JSON, for FOF CNF
 TPTP4X 0.0  s Utility for transforming and formatting