🚀 go-pugleaf

				   
			      AI SEMINAR
		     UNISYS PAOLI RESEARCH CENTER
				   

      Providing Modules and Lexical Scoping in Logic Programming

				Dale Miller
		      Computer and Information Science
			 University of Pennsylvania
			  Philadelphia, PA  19104

A first-order extension of Horn clauses, called first-order hereditary
Harrop formulas, possesses a meta theory which suggests that it would
make a suitable foundations for logic programming.  Hereditrary Harrop
formulas extended the syntax of Horn clauses by permitting
conjunctions, disjunctions, implications, and both existential and
universal quantifiers into queries and the bodies of program clauses.
A simple non-deterministic theorem prover for these formulas is known
to be complete with respect to intuitionistic logic.  This theorem
prover can also be viewed as an interpreter.  We shall outline how this
extended language provides the logic programming paradigm with a
natural notion of module and lexical scoping of constants.

				   
  		      2:00 pm Wednesday, April 6
		     Unisys Paloi Research Center
		      Route 252 and Central Ave.
			    Paoli PA 19311
				   
   -- non-Unisys visitors who are interested in attending should --
   --   send email to finin@prc.unisys.com or call 215-648-7446  --
				   
Tim Finin			finin@prc.unisys.com
Paoli Research Center		..!{psuvax1,sdcrdcf,cbmvax,bpa}!burdvax!finin
Unisys Corporation		215-648-7446 (o)  
PO Box 517, Paoli PA 19301	215-386-1749 (h)