June 2001
Intermediate to advanced
2128 pages
82h 43m
English
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.
Read now
Unlock full access