Options Settings

Option settings are of the form

$$\mbox{{\tt :- option(list(O)).}}$$

where

   O : term_size_weight | term_var_weight | term_var_weight_gt_small |
       normal_term_weight | increment(N) | var_depth(N) |
       special_relations(on) | special_relations(off) |
       ac(on) | ac(off) |
       memo_constraints(on) | memo_constraints(off)

The weight options set the weight function for terms and clauses which is used for inference selection.

term_ size_ weight

:

weight = number of nodes in a term

term_ var_ weight

weight = weighted product of term size, term depth and number of different variables

term_ var_ weight_ gt_ small

similar, except that ground terms are made very small

normal_ term_ weight

(default)

weight = weighted product of term size and depth

increment($N$)

Inferences are computed from clauses up to a certain weight. If no proof is found, the bound is increased by $N$. Defaults: $N = 15$ for term_ size_ weight, normal_ term_ weight, $N = 30$, otherwise.

var_ depth(N)

Clauses are preprocessed into rules in an order that also depends on the number of different variables occuring in it. If this number exceeds $N$ (default value is 3), processing of the clause is delayed.

special_ relations($S$)

$S=\mbox{{\tt on}}$ turns on the special treatment of transitive relations by chaining inferences; default. In this mode, transitivity, reflexivity, irreflexivity totality, density and no endpoint axioms are treated specifically. Saturate recognizes these properties automatically, provided they are not hidden, i.e., follow in a non-trivial way from other properties. Actually Saturate should be more clever in recognizing these properties.

$S=\mbox{{\tt off}}$: transitive relations are treated as any other predicate. This option should be specified textually before any axioms for the respective predicates. This option essentially reduces the inference system to ordered resolution. It should be used when Saturate is applied in order to prove the <locality of a Horn theory.

ac(S)

$S={\tt on}$ (default) results in employing AC-superposition based on AC-unification and extended rules for AC symbols.

$S=\mbox{{\tt off}}$ results in the treatment of AC-symbols by ordered rewriting.This option must textually preceed any AC laws.

memo_ constraints(S)

$S=\mbox{{\tt on}}$ switches memoization for ordering constraints on. This is the recommended setting for cases in which big ordering constraints are generated. This is the case in particular when clausal rewriting is turned on.

$S=\mbox{{\tt off}}$ (default): no memoization

option/1 may also be called interactively.

Imprint | Data Protection