Extending decidable clause classes via constraints

There are several well known possibilities which constrained clauses (= c-c lauses, for short) provide in addition to standard clauses. In particular, many (even infinitely many) standard clauses can be rep resented by a singl e c-clause. Hence, many parallel inference steps on standard clauses can be encoded in a single inference step on c-clauses. The aim of this work is t o investigate another possibility offered by constrained clauses: We shall try to combine resolution based decision procedures with constrained clause logic in order to increase the expressive power of the resulting decision classes. Therefore, there are two questions on which this paper focuses: 1. In what sense do constrained clauses actually provide additional express ive power in comparison with standard clauses? The answer given here is tha t only constraints made up from conjunctions of disequations constitute a g enuine extension w.r.t. standard clauses. 2. Is it possible to extend decision classes of standard clauses by the use of constrained clauses? The main result of this work is a positive answer to this question, namely a theorem which shows that standard clause classes decidable by certain resolution refinements remain decidable even if they are extended by constraints consisting of conjunctions of disequations. In order to prove the termination of our decision procedures on constrained clauses, some kind of compactness theorem for unification problems will be derived, thus extending a related result from [9].