final case class FormulaTerm(formula: Formula) extends Term with Product with Serializable
A formula in term position as used in TFX (FOOL logic). Terms of this kind can safely be ignored if TFX is not planned to be supported; and they will never be created by the leo.modules.input.TPTPParser for inputs that are non-TFX TFF formulas inputs.
- formula
The Formula in term position.
- Note
The leo.modules.input.TPTPParser will never yield expressions containing FormulaTerms that themself wrap single (formula) variables or atomic formulas, i.e., the expressions
FormulaTerm(FormulaVariable(x))
and
FormulaTerm(AtomicFormula(f, args))
are never created. Instead, an equivalent term expressions
Variable(x)
and
AtomicTerm(f, args)
, respectively, are created. This means that also for Boolean-typed variables or predicate applications, a representation as Term is returned. Of course, users may create such instances and handle them appropriately in their application.
- Alphabetic
- By Inheritance
- FormulaTerm
- Serializable
- Product
- Equals
- Term
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @native() @IntrinsicCandidate()
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- val formula: Formula
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @IntrinsicCandidate()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @IntrinsicCandidate()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @IntrinsicCandidate()
- def pretty: String
Returns a TPTP-compliant serialization of the term.
Returns a TPTP-compliant serialization of the term.
- Definition Classes
- FormulaTerm → Term
- def productElementNames: Iterator[String]
- Definition Classes
- Product
- def symbols: Set[String]
Returns a set of symbols (except variables) occurring in the term.
Returns a set of symbols (except variables) occurring in the term.
- Definition Classes
- FormulaTerm → Term
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
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