Back to the FAQ /
Several languages and systems are related to lambda Prolog. A few are
- 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.
- Designed as part of the thesis of Josh Hodas at UPenn, Lolli is
essentially the result of adding to lambda Prolog the linear
- 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.
- 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
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.
- Part of the
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.
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).
Back to the FAQ /