## 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 language | English (US) |
---|---|

Title of host publication | Unknown Host Publication Title |

Publisher | IEEE |

Pages | 379-388 |

Number of pages | 10 |

ISBN (Print) | 0818607998 |

State | Published - 1987 |