This is the documentation for the Scala TPTP parser used, e.g., by the Leo-III prover.
This is the documentation for the Scala TPTP parser used, e.g., by the Leo-III prover.
Package structure
The leo package contains two sub-packages as follows:
leo.datastructures contains the leo.datastructures.TPTP object
that bundles the different abstract syntax tree (AST) representations for the different TPTP
language dialects, including ...
This is the documentation for the Scala TPTP parser used, e.g., by the Leo-III prover.
Package structure
The leo package contains two sub-packages as follows:
leo.datastructures
contains the leo.datastructures.TPTP object that bundles the different abstract syntax tree (AST) representations for the different TPTP language dialects, including ...leo.datastructures.TPTP.THF
- Higher-order formulas (THF)leo.datastructures.TPTP.TFF
- Typed first-order formulas (TFF)leo.datastructures.TPTP.FOF
- Untyped first-order formulas (FOF)leo.datastructures.TPTP.TCF
- Typed clausal form (TCF)leo.datastructures.TPTP.CNF
- Untyped clausal form (CNF)leo.modules.input
- the parser itself.Usage (in short)
The leo.modules.input.TPTPParser offers several parsing methods:
Exemplary use case