System
| CPU s
| Transform
| Format
| Command
| Application
|
AGInTRater 0.0
|
s
|
|
|
|
Rates proof formulae for interestingness, for
|
AGMV 1.0
|
s
|
|
|
|
Model verifier, for NX0 TX0 TF0 FOF
|
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
|
GAPT 2.16.0
|
s
|
|
|
|
Derivation verifier, for FOF CNF
|
GDV 1.0
|
s
|
|
|
|
Derivation verifier, for TH0 TX0 TF0 FOF CNF
|
GDV‑LP 1.0
|
s
|
|
|
|
Derivation verifier for LambdaPi format, for TH0 TF0 FOF CNF
|
IDV 0.0
|
s
|
|
|
|
Interactive derivation viewer
|
IIV 0.0
|
s
|
|
|
|
Interactive interpretation viewer
|
InterpretByATP 0.0
|
s
|
|
|
|
Evaluates formulae against a model, between SZS lines (ask Geoff)
|
PProofSummary 0.0
|
s
|
|
|
|
Summarizes proof in Prolog format
|
ProofSummary 0.0
|
s
|
|
|
|
Summarizes proof
|
SolutionStats 1.0
|
s
|
|
|
|
Print solution statistics
|
TPTP2JSON 0.1
|
s
|
|
|
|
Converts to JSON, for FOF CNF
|
TPTP4X 0.0
|
s
|
|
|
|
Utility for transforming and formatting
|