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:

  • 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:

  • leo.modules.input.TPTPParser.problem - for a whole TPTP problem
  • leo.modules.input.TPTPParser.annotated - for an annotated TPTP formula (specialized methods for the individual dialects exist).
  • leo.modules.input.TPTPParser.thf - for a plain THF formula (without annotations)
  • leo.modules.input.TPTPParser.tff - for a plain TFF formula (without annotations)
  • ... etc.

  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

•  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:

  • THF formulas are parsed into datastructures.TPTP.THF,
  • TFF formulas are parsed into datastructures.TPTP.TFF,
  • FOF/TPI formulas are parsed into datastructures.TPTP.FOF,
  • TCF formulas are parsed into datastructures.TPTP.TCF, and
  • CNF formulas are parsed into datastructures.TPTP.CNF.

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

  • Annotated THF formulas wrapped as datastructures.TPTP.THFAnnotated,
  • Annotated TFF formulas wrapped as datastructures.TPTP.TFFAnnotated,
  • Annotated FOF formulas wrapped as datastructures.TPTP.FOFAnnotated,
  • Annotated TCF formulas wrapped as datastructures.TPTP.TCFAnnotated,
  • Annotated CNF formulas wrapped as datastructures.TPTP.CNFAnnotated, and
  • Annotated TPI formulas wrapped as datastructures.TPTP.TPIAnnotated.

  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.

  Definition Classes

  input

  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.

• TPTPLexer
• TPTPParseException
• TPTPParser

leo.modules.input.TPTPParser

TPTPLexer

Companion object TPTPLexer