[comp.theory] Question on Restricted Quantification Logic

ahudli@silver.ucs.indiana.edu (anand hudli) (04/14/90)

Many-sorted Unification has been a well studied problem. In many sorted
logic, variables and domains and ranges of functions are restricted to
certain subsets of the universe. It has also been shown that a proof 
by resolution in the many-sorted case can be much shorter than a 
proof by resolution in the usual first order logic.  A related formalism 
is the theory of Restricted Quantification (Hailperin " A theory of
 Restricted Quantification", Journal of Symbolic Logic, 1957). In 
 this logic, variables are restricted to sets of elements that 
 satisfy certain properties, where each property is specified as
a predicate. 

 I have two questions :
 
	1) Can Restricted Quantification theory find application
	in logic Programming or AI ? If so could you give me some
	examples where it could be useful ? 

	2) Has any work been done in Unification in Restricted
	Quantification Theory? 


 Thanks . 

 Anand Hudli
 ahudli@silver.ucs.indiana.edu