Path: utzoo!attcan!uunet!cs.utexas.edu!mailrus!iuvax!silver!ahudli
From: ahudli@silver.ucs.indiana.edu (anand hudli)
Newsgroups: comp.ai
Subject: Question on Restricted Quantification Theory
Message-ID: <41824@iuvax.cs.indiana.edu>
Date: 13 Apr 90 21:12:40 GMT
Sender: root@iuvax.cs.indiana.edu
Organization: Indiana University, Bloomington IN.
Lines: 27



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