= 768" x-on:close-sidebar="sidebar=window.innerWidth >= 768 && true">
package dolmen
-
dolmen
-
dolmen.intf
-
-
dolmen.line
-
dolmen.smtlib2
-
dolmen.std
-
-
dolmen.tptp
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
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