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

No credit card required

### 5.3 Refutational Completeness

We establish the refutational completeness of general ordered resolution by showing that the calculus has the reduction property for counterexamples. We essentially use the model functor I from Definition 3.14, but applied to general clauses and with an additional restriction on productive clauses.

Let N be a set of general clauses and be an admissible ordering. We use induction on to define, for each clause $C$ , a Herbrand interpretation I C and a set ε C as follows.

5.2

Definition

Take I C to be ...

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

No credit card required