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.