module type Statement = sig .. end
type
The type of statements.
type
The type of identifiers
type
The type of terms used in statements.
type
The type of locations attached to statements.
val annot : ?loc:location ->
term ->
term list -> term
Terms as annotations for statements.
val include_ : ?loc:location ->
string -> id list -> t
Include directive. Given the filename, and a list of
names to import (an empty list means import everything).
val tpi : ?loc:location ->
?annot:term ->
id ->
string -> term -> t
val thf : ?loc:location ->
?annot:term ->
id ->
string -> term -> t
val tff : ?loc:location ->
?annot:term ->
id ->
string -> term -> t
val fof : ?loc:location ->
?annot:term ->
id ->
string -> term -> t
val cnf : ?loc:location ->
?annot:term ->
id ->
string -> term -> t
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 1assert (not t)check_satpop 1assert 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