Expand description
Syntax trees
Structs
Formula annotations
A CNF formula
Enums
A CNF literal
An associative binary operator on FOF formulae
A FOF formula
A non-associative binary operator on FOF formulae
A FOF quantifier
A FOF term.
A unary operator on FOF formulae
A TPTP formula role, such as
axiom or negated_conjectureAn infix binary operator on FOF terms
One of various types of TPTP identifiers.
Formula sources for use in annotations
A top-level TPTP statement, currently
include, cnf, or fof.