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 datastructures
    Definition Classes
    leo
  • TPTP
  • package modules
    Definition Classes
    leo
p

leo

datastructures

package datastructures

Ordering
  1. Alphabetic
Visibility
  1. Public
  2. Protected

Value Members

  1. object TPTP

    Collection of TPTP-related data types that are returned by the leo.modules.input.TPTPParser.

    Collection of TPTP-related data types that are returned by the leo.modules.input.TPTPParser. An overview:

    See TPTP.THF, TPTP.TFF, TPTP.FOF, TPTP.TCF, TPTP.CNF for more information on the representation of "plain" THF, TFF, FOF, TCF and CNF formulas, respectively.

    All classes have a function called pretty that will output the TPTP-compliant representation of the respective structure. It should hold that parse(x.pretty) = x where parse is the hypothetical parsing function for that structure.

Ungrouped