Bürckert extends and unifies various theories about constrained quantifiers (such as sorted resolution, theory unification, and theory resolution) as applied to resolution  theorem  proving. The idea is to allow general formulas over a general theory to be used as the restrictions on quantified variables, rather than using restrictions that are just simple type names, as in simple sorted logics. The general inference technique is described, and an extension to Herbrand’s theorem is proven. The paper presents a good discussion of completeness issues for constrained quantifier systems as well as a good (and honest) discussion of the difficulties arising from the most general forms of the new constrained inference technique. Some theoretical results about simplifying constraints are also given.

The author does not discuss the relative effectiveness of such general constrained inference systems as compared with, say, ordinary sorted logic or theory resolution in actual running programs. He makes it clear, however, that the purpose of this paper is to provide the theoretical background, and does not make claims about the efficacy of inference programs based on the new technique. The presentation is concise and deeply theoretical. It is accessible with moderate difficulty to anyone familiar with ordinary resolution theory. I would have found the paper much easier to follow if it had used more example problems in which the formulas were completely written out and the inferences spelled out in detail.