Back to the FAQ /
Home
Related Systems
Several languages and systems are related to lambda Prolog. A few are
listed below.
 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
goaldirected 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.
 Llambda
 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 LambdaAbstraction, 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 higherorder hereditary formulas. As
a result, Isabelle implements both the unification of simply typed
lambdaterms as well as clausal resolution. While control in lambda Prolog
is governed by depthfirst 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 higherorder specification language based on the LF Logical Framework (a
dependenttyped lambdacalculus). It is intended as a uniform
metalanguage 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).
Back to the FAQ /
Home