Imagining CLP(Λ,≡αβ)

. We study under which conditions the domain of -terms () and the equality theory of the -calculus (j fffi ) form the basis of a usable constraint logic programming language (CLP). The conditions are that the equality theory must contain axiom j, and the formula language must depart from Horn clauses and accept universal quantifications and implications in goals. In short, CLP(, j fffi ) must be close to Prolog. 1 Introduction Logic programming is a programming paradigm in which programs are logical formulas, and executing them amounts to search for a proof. The most famous practical incarnation of logic programming is Prolog, which is based on Horn formulas [31]. The formalism of Horn programs is computationally complete [1, 49], but one has often tried to augment it to gain more flexibility and expressivity. One of these attempts is the paradigm of constraint logic programming [11, 27, 10, 50]. It amounts to replacing unification of first-order terms, considered as a procedure for s..