Completeness and redundancy in constrained clause logic

In [6], a resolution-based inference system on c-clauses (i.e. constrained clauses) was introduced, incorporating powerful deletion rules for redundan cy elimination. This inference system was extended to resolution refinement s in subsequent papers of Caferra et al. (e.g. [4] and [5]). The completene ss proofs given for the purely refutational calculi (i.e.: the inference sy stems without deletion rules) are basically "translations" of the correspon ding results from standard clause logic to constrained clause logic (= c-cl ause logic, for short). This work focuses on the deletion rules of the calculi of Caferra et al. an d, in particular, on the c-dissubsumption rule, which is considerably more powerful than the usual subsumption concept in standard clause logic. We wi ll. show that the "conventional" method for proving the completeness of (st andard clause) resolution refinements with subsumption fails when the power ful deletion rules of Caferra et al. are considered. Therefore, in order to prove the completeness of the c-clause calculi, a different strategy is re quired. To this end, we shall extend the well-known concept of semantic tre es from standard clause logic to c-clause logic. In general, purely non-det erministic application of the inference rules is not sufficient to ensure r efutational completeness. It is intuitively clear, that some sort of "fairn ess" must be required. The completeness proof via semantic trees gives us a hint for defining precisely what it means for a rule application strategy to be "fair". Finally other methods for proving completeness and defining redundancy crit eria are contrasted with completeness via semantic trees and c-dissubsumpti on. In particular, it is shown that the redundancy criteria within the orde ring-based approaches of Bachmair/Ganzinger (cf. [2]) and Nieuwenhuis/Rubio (cf. [11]) are incomparable with c-dissubsumption.