Redundancy

Proving the redundancy of clauses and inferences is indispensible for pruning the search space non-locally. With the techniques that are implemented in Saturate we can effectively compute saturated sets of clauses in more cases than with most other saturation-based provers. Finite, saturated sets of clauses not containing the empty clause are provably consistent, and more efficient refutational theorem proving strategies become available for proving consequences of such theories. Sometimes they provide the basis for a decision procedure for the respective theory.

Redundany is closely tied to the term ordering that one uses. In short, a clause is redundant in a particular state of the saturation process if it is logically entailed by smaller clauses that exist in that state. For inferences a similar criterion applies: if the conclusion is entailed by clauses smaller than the negative premise it is redundant (see (Bachmair & Ganzinger, 1994 b). Ordering constraints as they arise from inferences can be kept with the conclusion and inherited to its descendants as described in (Nieuwenhuis & Rubio, 1992 a) and (Nieuwenhuis & Rubio, 1992 b). This technique not only provides for a more precise checking of the constraints, it also increases the power in checking for redundancy of inferences.

Imprint | Data Protection