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
, a Herbrand interpretation I
C
and a set ε
C
as follows.
Get Handbook of Automated Reasoning now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
