The type of statements.

Terms as annotations for statements.

Include directive. Given the filename, and a list of names to import (an empty list means import everything).

TPTP statements, used for instance as tff ~loc ~annot name role t. Instructs the prover to register a new directive with the given name, role and term. Current tptp roles are:

• "axiom", "hypothesis", "definition", "lemma", "theorem" acts as new assertions/declartions

• "assumption", "conjecture" are proposition that need to be proved, and then can be used to prove other propositions. They are equivalent to the following sequence of smtlib statements:

  • push 1
  • assert (not t)
  • check_sat
  • pop 1
  • assert t
• "negated_conjecture" is the same as "conjecture", but the given proposition is false (i.e its negation is the proposition to prove).
• "type" declares a new symbol and its type
• "plain", "unknown", "fi_domain", "fi_functors", "fi_predicates" are valid roles with no specified semantics
• any other role is an error