Packages

  • package root

    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:

    Usage (in short)

    The leo.modules.input.TPTPParser offers several parsing methods:

    Exemplary use case 

    import leo.modules.input.{TPTPParser => Parser}
import TPTPParser.TPTPParseException
import leo.datastructures.TPTP.THF

try {
 val result = Parser.problem(io.Source.fromFile("/path/to/file"))
 println(s"Parsed ${result.formulas.size} formulae and ${result.includes.size} include statements.")
 // ...
 val annotatedFormula = Parser.annotatedTHF("thf(f, axiom, ![X:$i]: (p @ X)).")
 println(s"${annotatedFormula.name} is an ${annotatedFormula.role}.")
 // ...
 val formula = Parser.thf("![X:$i]: (p @ X)")
 formula match {
   case THF.FunctionTerm(f, args) => // ...
   case THF.QuantifiedFormula(quantifier, variableList, body) => // ...
   case THF.Variable(name) => // ...
   case THF.UnaryFormula(connective, body) => // ...
   case THF.BinaryFormula(connective, left, right) => // ...
   case THF.Tuple(elements) => // ...
   case THF.ConditionalTerm(condition, thn, els) => // ...
   case THF.LetTerm(typing, binding, body) => // ...
   case THF.DefinedTH1ConstantTerm(constant) => // ...
   case THF.ConnectiveTerm(conn) => // ...
   case THF.DistinctObject(name) => // ...
   case THF.NumberTerm(value) => // ...
 }
 // ...
} catch {
 case e: TPTPParseException => println(s"Parse error at line ${e.line}:${e.offset}: ${e.getMessage}")
}
    Definition Classes
    root
  • package leo
    Definition Classes
    root
  • package modules
    Definition Classes
    leo
  • package input
    Definition Classes
    modules
  • TPTPParser

package input

Ordering
  1. Alphabetic
Visibility
  1. Public
  2. Protected

Value Members

  1. object TPTPParser

    Parser for TPTP-based input languages for automated theorem proving, including ...

    Parser for TPTP-based input languages for automated theorem proving, including ...

    • THF (TH0/TH1): Monomorphic and polymorphic higher-order logic,
    • TFF (TF0/TF1): Monomorphic and polymorphic typed first-order logic, including extended TFF (TFX),
    • FOF: Untyped first-order logic,
    • TCF: Typed clause-normal form,
    • CNF: (Untyped) clause-normal form, and
    • TPI: TPTP Process Instruction language.

    Both annotated as well as "plain" (meant here: not annotated) formulas can be read. An annotated formula (here, as an example: annotated THF formula) is of form thf(name, role, formula, annotations) whereas the plain formula is the formula part of this instance.

    The parser translated plain formulas into an abstract syntax tree defined at datastructures.TPTP, resp. its corresponding specializations for the respective language dialect:

    Annotated formulas are additionally wrapped in an datastructures.TPTP.AnnotatedFormula object as follows:

    Whole TPTP files are represented by datastructures.TPTP.Problem objects. Note that include directives etc. are parsed as-is and are represented by an datastructures.TPTP.Include entry in the datastructures.TPTP.Problem representation. In particular, they are not parsed recursively. This has to be implemented externally (e.g., by recursive calls to the parser).

    Parsing errors will cause TPTPParser.TPTPParseExceptions.

    Since

    January 2021

    Note

    For the original implementation of this parser v7.4.0.3 of the TPTP syntax was used, but it's being updated constantly to keep track with TPTP language updates.

    See also

    Original TPTP syntax definition at http://tptp.org/TPTP/SyntaxBNF.html.

Ungrouped