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
|
Dedukti 2.7
|
s
|
|
|
|
Derivation verifier, for TH0 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 with LambdaPi check, 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)
|
LambdaPi 2.5.0
|
s
|
|
|
|
LambdaPi for GDV files, for TH0 TF0 FOF CNF
|
OAESys 0.0
|
s
|
|
|
|
Extracts answers from derivation
|
OAFSys 0.0
|
s
|
|
|
|
Extracts answers from derivation, with reproving
|
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
|