Handbook of Automated Reasoning

4 Saturation procedures

The completeness results presented until now only apply to closure procedures, that is, deduction procedures which compute the closure of an initial set of clauses under a given inference system, without considering simplification or deletion techniques. However, such techniques are well-known to be crucial for efficiency in paramodulation-based theorem proving. In this section we study their compatibility with refutation completeness.

4.1 Redundancy in practice

Let us first give some examples of practical simplification and deletion methods. Most provers apply these methods in two possible contexts. The first one, usually called forward redundancy elimination, is applied to new clauses immediately after they are ...