hide
Free keywords:
-
Abstract:
We modify Bezem's (Bezem, M. Completeness of
Resolution Revisited. Theoretical Computer
Science 74 (1990) 227-237) completeness proof
for ground resolution in order to
deal with ordered resolution, redundancy,
and equational reasoning in form
of superposition. The resulting proof is
completely independent of the
cardinality of the set of clauses.