Back to the FAQ / Home

• Languages designed on proof theoretic considerations Lambda Prolog is an extension of Horn clause logic programming based on simple proof theory consideration of completeness with respect to goal-directed search. There are two other languages that have been similarly motivated and which are related closely to lambda Prolog.

  Lolli

  Designed as part of the thesis of Josh Hodas at UPenn, Lolli is essentially the result of adding to lambda Prolog the linear logic implication.

  Forum

  This is a way to view all of linear logic as a logic programming language. Forum modularly extends the logical foundations of both lambda Prolog and Lolli.

  L-lambda

  This is a subset of lambda Prolog in which the unification of lambda terms is decidable and for which most general unifiers exist when unifiers exist. This language is described in the following paper.

  A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification, by Dale Miller. Journal of Logic and Computation, Vol. 1, No. 4 (1991), 497 -- 536. (DVI) (Postscript)

• Part of the Isabelle theorem proving system is a fragment of higher-order hereditary formulas. As a result, Isabelle implements both the unification of simply typed lambda-terms as well as clausal resolution. While control in lambda Prolog is governed by depth-first search, control is Isabelle is governed by a large and specialized set of tactics and tacticals in the LCF tradition. This system is used for the specification of logics and theorem provers.

• Twelf is a higher-order specification language based on the LF Logical Framework (a dependent-typed lambda-calculus). It is intended as a uniform meta-language for specifying, implementing, and proving properties of programming languages and logics. There are many similarities between Elf and lambda Prolog, although the source languages different significantly (logic versus type theory).