O'Reilly logo

Handbook of Automated Reasoning by Andrei Voronkov, Alan J.A. Robinson

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required