Default: autoSpecifies 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. Provable equivalence is defined as the syntactic equality of two terms. maedmax : Uses the maedmax prover. Must be installed. 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.

Keyword:

chase

coequalize

eval

pi

import_jdbc_all

schema_literal

colimit

unit

coeval

sigma

pi

typeside_literal

counit_query

sigma

import_jdbc

query_literal

unit_query

coproduct

counit

simple

import_jdbc_all

instance_literal

toCoQuery

constraints_literal

Appears in:

All_Syntax

Employees

KB

Tutorial