Publikation
On Skolemization in Constrained Logics
Hans-Jürgen Bürckert; Bernhard Hollunder; Armin Laux
In: Martin C. Golumbic (Hrsg.). Annals of Mathematics and Artificial Intelligence (AMAI), Vol. 18, No. 2, Pages 95-131, Springer, Netherlands, 9/1996.
Zusammenfassung
Quantification in first-order logic always involves all elements of the universe. However, it is often more natural to just quantify over those elements of the universe which satisfy a certain condition. Constrained logics therefore provide restricted quantifiers X:R F and X:R F whereX is a set of variables, and which can be read as F holds for all elements satisfying the restrictionR and F holds if there exists an element which satisfiesR. In order to test satisfiability of a set of such formulas by means of an appropriately extended resolution principle, one needs a procedure which transforms them into a set of clauses with constraints. Such a procedure essentially differs from the classical transformation of first-oder formulas into a set of clauses, in particular since quantification over the empty set may occur and since the needed Skolemization procedure has to take the restrictions of restricted quantifiers into account. In the first part of this article we present a procedure that transforms formulas with restricted quantifiers into a set of clauses with constraints while preserving satisfiability. The thus obtained clauses are of the formC R whereC is an ordinary clause andR is a restriction, and can be read as C holds ifR holds. These clauses can now be tested on unsatisfiability via the existingconstrained resolution principle. In the second part we generalize the constrained resolution principle in such a way that it allows for further optimization, and we introduce a combination of unification and constraint solving that can be employed to instantiate this kind of optimization.