sass: Choosing a Selection Strategy

$$\mbox{{\tt sass}}$$

specifying the Selection Strategy. Selection has a similar meaning as in SLD-resolution. Selection is, in addition to the reduction ordering, the second main parameter to the chaining and paramodulation inference systems.

One may choose from 4 alternatives. sass([]) turns selection off, resulting in a fully ordered strategy. sass([$F$]) specifies one of three selection strategies:

$F=1$:

(default) automatic selection of a maximal literal in non-reductive clauses

$F=2$:

automatic selection of a small literal in non-positive clauses

$F=3$:

user guided literal selection

Option $F=3$ is the one where the user is asked interactively for each non-positive clause to select a negative literal for chaining and superposition.

In option $F=1$ which is fully automatic, no negative literal is selected if the clause has a positive literal which is strictly greater than all negative literals. Otherwise one, usually maximal, negative literal is selected.

Option $F=2$ always selects a (if possible non-maximal) literal in any non-positive clause. This results in a positive strategy.

The system indicates, by printing an asterix ``*'', those clauses for which a literal has been selected. The selected literal is listed first in the antecedent.

Option $F=1$ sounds like applying usual ordering constraints to inferences. It is different in that we now perform all negative chainings into the selected literal, even in cases where the substituted literal (after applying the unifier of the inference) is not maximal. What we gain is that we never need to chain from that clause. Moreover the ordering constraints are simpler and hence faster to check.

This strategy seems to work better than the fully ordered strategy most of the time. Highly recommended in cases where clauses are too long to admit full checking of ordering constraints.

sass has been called sama in earlier versions of Saturate.

Imprint | Data Protection