final case class FOFAnnotated(name: String, role: String, formula: Statement, annotations: Annotations) extends AnnotatedFormula with Product with Serializable
An annotated FOF formula.
- Alphabetic
- By Inheritance
- FOFAnnotated
- Serializable
- Product
- Equals
- AnnotatedFormula
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new FOFAnnotated(name: String, role: String, formula: Statement, annotations: Annotations)
Type Members
- type F = Statement
The type of the wrapped formula.
The type of the wrapped formula.
- Definition Classes
- FOFAnnotated → AnnotatedFormula
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
- val annotations: Annotations
The annotations of the annotated formula, if any.
The annotations of the annotated formula, if any.
- Definition Classes
- FOFAnnotated → AnnotatedFormula
- 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: Statement
The underlying formula of the annotated formula.
The underlying formula of the annotated formula.
- Definition Classes
- FOFAnnotated → AnnotatedFormula
- def formulaType: FormulaType
The AnnotatedFormula.FormulaType of the underlying formula.
The AnnotatedFormula.FormulaType of the underlying formula.
- Definition Classes
- FOFAnnotated → AnnotatedFormula
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @IntrinsicCandidate()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- val name: String
The name of the annotated formula.
The name of the annotated formula.
- Definition Classes
- FOFAnnotated → AnnotatedFormula
- 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 formula.
Returns a TPTP-compliant serialization of the formula.
- Definition Classes
- FOFAnnotated → AnnotatedFormula
- def productElementNames: Iterator[String]
- Definition Classes
- Product
- val role: String
The role of the annotated formula.
The role of the annotated formula.
- Definition Classes
- FOFAnnotated → AnnotatedFormula
- def symbols: Set[String]
Contains every constant symbol (i.e., no variables) occurring in the formula, including term and type symbols.
Contains every constant symbol (i.e., no variables) occurring in the formula, including term and type symbols.
- Definition Classes
- FOFAnnotated → AnnotatedFormula
- 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