option prover
Default: auto
Specifies which theorem prover to use. The prover string should come from the list below. Only the completion method has options. Note that these theorem proving methods are not ``java aware''; to use java typesides, instances ``wrap'' these provers with java simplification. Provers are:
auto : The auto theorem proving method attempts the free, congruence, monoidal, and program methods, in that order.
completion : Applies unfailing (ordered) Knuth-Bendix completion specialized to lexicographic path ordering. If no completion precedence is given, attempts to infer a precedence using constraint-satisfaction techniques.
congruence : Applies only to ground (variable-free) theories. Uses the classical Nelson-Oppen congruence-closure-with-union-find algorithm.
e : Uses the E prover. Must be installed.
fail : Applies to all theories. Always fails with an exception.
free : Applies only to theories without equations. Equivalence is implemented as the syntactic equality of two terms.
monoidal : Applies to theories where all equations are monadic (unary) or ground. Applies Knuth-Bendix completion specialized to semi-Thue systems.
program : Applies only to weakly orthogonal theories. Interprets all equations p = q as rewrite rules p -> q if p is syntactically smaller than q and q -> p if q is syntactically smaller than p and symbolically evaluates terms to normal forms. Fails if an equation cannot be oriented.
vampire : Experimental.
Keyword:
coequalize
eval
pi
import_jdbc_all
schema_literal
colimit
counit
unit_query
pi
sigma
typeside_literal
counit_query
include
sigma
import_jdbc_direct
import_jdbc
query_literal
back
coeval
coproduct
unit
constraints_literal
simple
instance_literal
toCoQuery
chase
Appears in:
All_Syntax
Employees
KB
NewDemo
NewDemoPsuedo
Stdlib
Tutorial