A resolution principle for constrained logics

摘要

We introduce a constrained logic scheme with a resolution principle for clauses whose variables are constrained by a constraint theory. Constraints can be seen as quantifier restrictions filtering out the values that any interpretation of the underlying constraint theory can assign to the variables of a formula with such restricted quantifiers.