Rewriting and reasoning with set-relations II: The non-ground case completeness

Abstract

We consider reasoning and rewriting with set-relations: inclusion, nonempty intersection and singleton identity, each of which satisfies only two among the three properties of the equivalence relations. The paper presents a complete inference system which is a generalization of ordered paramodulation and superposition calculi. Notions of rewriting proof and confluent rule system are defined for such non-equivalence relations. Together with the notions of forcing and redundancy they are applied in the completeness proof. Ground completeness cannot be lifted to the non-ground case because substitution for variables is restricted to deterministic terms. To overcome the problems of restricted substitutivity and hidden (in relations) existential quantification, unification is defined as a three step process: substitution of determistic terms, introduction of bindings and "on-line" skolemisation. The inference rules based on this unification derive non-ground clauses even from the ground ones, thus making an application of a standard lifting lemma impossible. The completness theorem is proved directly without use of such a lemma.