LOGIC PROGRAMMING APPROACH TO MANIPULATING FORMULAS AND PROGRAMS.

Dale Miller, Gopalan Nadathur

Research output: Chapter in Book/Report/Conference proceedingConference contribution

53 Scopus citations

Abstract

By permitting function and predicate symbols to be variables and by replacing first-order terms by simply typed lambda -terms, a higher-order extension to first-order Horn clauses can be described. To be complete in principle, a logic-programming language based on this extension must incorporate higher order unification. Although this is a more complex operation than first-order unification, its availability as a primitive makes certain kinds of programming tasks easier. This aspect is illustrated by presenting some programs in a higher-order version of Prolog called lambda Prolog that manipulate objects, such as formulas and programs, whose representation requires structures containing abstractions or bound variables. It is shown how a simple natural deduction theorem prover may be implemented in lambda Prolog and how some simple program transformers for a functional programming language may be written in this language.

Original languageEnglish (US)
Title of host publicationUnknown Host Publication Title
PublisherIEEE
Pages379-388
Number of pages10
ISBN (Print)0818607998
StatePublished - Dec 1 1987

Fingerprint Dive into the research topics of 'LOGIC PROGRAMMING APPROACH TO MANIPULATING FORMULAS AND PROGRAMS.'. Together they form a unique fingerprint.

Cite this