[−][src]Module tptp::syntax
Parsed syntactic structures
Structs
Annotations | Formula annotations |
CnfFormula | A CNF formula |
Included | An include path, not including outer quotes |
Variable | A variable name, |
Enums
AssocConnective | An associative binary operator on FOF formulae |
CnfLiteral | A CNF literal |
DagSource | DAG formula sources |
ExternalSource | External formula sources |
FofFormula | A FOF formula |
FofQuantifier | A FOF quantifier |
FofTerm | A FOF term. |
FormulaRole | A TPTP formula role, such as |
InfixEquality | An infix binary operator on FOF terms |
InternalSource | Internal formula sources |
Name | One of various types of TPTP identifiers. |
NonAssocConnective | A non-associative binary operator on FOF formulae |
Source | Formula sources for use in annotations |
Statement | A top-level TPTP statement, currently |
UnaryConnective | A unary operator on FOF formulae |