- Authors:
- Gopalan Nadathur,
- Dale Miller
$\lambda$Prolog is a logic programming language that extends Prolog by incorporating notions of higher-order functions, $\lambda$-terms, higher-order unification, polymorphic types, and mechanisms for building modules and secure abstract data types. These new features are provided in a principled fashion by extending the classical first-order theory of Horn clauses to the intuitionistic higher-order theory of {\em hereditary Harrop} formulas. The justification for considering this extension a satisfactory logic programming language is provided through the proof-theoretic notion of a {\em uniform proof}. The correspondence between each extension to Prolog and the new features in the stronger logical theory is discussed. Also discussed are various aspects of an experimental implementation of $\lambda$Prolog.
Recommendations
Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf
$\lambda$Prolog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a great economy of expression. We encode a higher-order logic using an ...
Mathematical Induction in Otter-Lambda
Otter-lambda is Otter modified by adding code to implement an algorithm for lambda unification. Otter is a resolution-based, clause-language first-order prover that accumulates deduced clauses and uses strategies to control the deduction and retention ...
Lambda Abstraction Algebras: Coordinatizing Models of Lambda Calculus
Lambda abstraction algebras are designed to algebraize the untyped lambda calculus in the same way cylindric and polyadic algebras algebraize the first-order logic; they are intended as an alternative to combinatory algebras in this regard. Like ...