LOGIC PROGRAMMING APPROACH TO MANIPULATING FORMULAS AND PROGRAMS.

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.