On skolemization in constrained logics

Abstract

First-order logics allows one to quantify over all elements of the universe. However, it is often more natural to quantify only over those elements which satisfy a certain condition. Constrained logics provide this possibility by introducing restricted quantifiers ∀ X:R F and ∃ X:R F where X is a set of variables, and which can be read as "F holds for all elements satisfy R", respectively. In order to test unsatisfiability of a set of such formulas using an extended resolution principle, one needs a procedure which transforms them into a set of constrained clauses. Such a procedure causes more problems than the classical transformation of first-order formulas into a set of clauses. This is due to the fact that quantification over the empty set may occur. Especially, a modified Skolemization procedure has to be used in order to remove restricted existential quantifiers. In this paper we will give a procedure that transforms formulas with restricted quantifiers into a set of clauses with constraints preserving unsatisfiability. Since restrictions may be given by sorts this procedure can, e.g., be applied to sorted logics where empty sorts may occur. The obtained clauses are of the form C || R where C is an ordinary clause and R is a restriction, and which can be read as "C holds if R holds". They can be tested on unsatisfiability via constrained resolution. Finally, we introduce so-called constraint unification which can be used for optimization of constrained resolution if certain conditions are satisfied.