sair: Settings for Inference Rules

$$\mbox{{\tt sair}}$$

This flag lists the set of inference rules $R$ that are to be applied fairly to persisting clauses.

The rules are identified by numbers as follows:

$R=1$:

reflexivity resolution

$R=2$:

right superposition and chaining

$R=3$:

left superposition and negative chaining

$R=4$:

factoring

$R=5$:

ordered resolution

$R=6$:

transitivity resolution

$R=7$:

tableau expansion

The inference system consisting of all theses rules is refutationally complete In the case of dense orderings, one additionally needs to switch on variable elimination for refutational completeness, cf. command saes. The default setting is determined by the current theory and assures that sufficiently many inference rules are turned on. Transitivity resolution is only needed for specific cases of transitive relations.

It is a good strategy (with respect to time efficiency) to set active inferences according to the problem at hand; for instance, for a purely equational problem only inference 3 (right superposition) is needed.

The inference system can be further instantiated with strategies for

1. constraint inheritance: command saci
2. selecting negative literals: command sass, and
3. eager simplifications: command saes.

For a description of these inferences we refer to our overview and to (Bachmair & Ganzinger, 1995 b).

Imprint | Data Protection