finin@antares.PRC.Unisys.COM (Tim Finin) (04/05/88)
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)