saci: Settings for Constraint Inheritance

$$\mbox{{\tt saci}}$$

specify the setting of the constraint Inheritance strategy. The (pairwise exclusive) options $O$ for constraint inheritance are

$O=1$:

no constraint inheritance but complete immediate checking (default),

$O=2$:

hereditary ordering constraint,

$O=3$:

hereditary equality constraint: basic strategies.

With option 1 one gets a complete checking of ordering constraints with each inference.

With option 2, ordering constaints are inherited from the premises to the conclusion of an inference, enriched by the ordering constraint for that inference. In this case ordering constraints may become prohibitively large. Constraints are only inherited for non-unit clauses. No constraint weakening is performed. That is, even when $C$ subsumes $D$ but the constraint of $D$ does not imply the constraint of $C$, $D$ will not be deleted. An alternative would be to delete $D$, and at the same time weaken the constraint for $C$ such that the weaker constraint is implied.

Option 3 is incompletely implemented and should not be used at present.

If all options are turned off by calling saci([]) clauses are preoriented once and for all, and inferences are computed with maximal literals and terms according to this preorientation. This corresponds to checking ordering constraints before the unfier is applied. If big clauses are produced during saturation, solving ordering constraints may be prohibitively expensive and saci([]) might be a good choice.

Imprint | Data Protection