A Resolution Principle for a Logic with Restricted Quantifiers

This monograph presents foundations for a constrained
logic scheme treating constraints as a very general form of
restricted quantifiers. The constraints - or quantifier
restrictions - are taken from a general constraint system
consisting of constraint theory and a set of distinguished
constraints.
The book provides a calculus for this constrained logic
based on a generalization of Robinson's resolution
principle. Technically, the unification procedure of the
resolution rule is replaced by suitable constraint-solving
methods. The calculus is proven sound and complete for the
refutation of sets of constrained clauses. Using a new and
elegant generalization of the notion ofa ground instance,
the proof technique is a straightforward adaptation of the
classical proof technique.
The author demonstrates that the constrained logic scheme
can be instantiated by well-known sorted logics or
equational theories and also by extensions of predicate
logics with general equational constraints or concept
description languages.