In this report we introduce a new proof-theoretic approach to the semantics of Constraint Logic Programming, based on an intuitionistic first-order modal logic, called QLL. The distinguishing feature of this new approach is that the logic calculus of QLL is used not only to capture the usual extensional aspects of Logic Programming, i.e. ``which queries are successful,'' but also some of the intensional aspects, i.e. ``what is the answer constraint and how is it constructed.'' It provides for a direct link between the model-theoretic and the operational semantics following a formulas-as-programs and proofs-as-constraints principle.
This approach makes use of logic in a different way than other approaches based on logic calculi. On the one side it is to be distinguished from the well-known provability semantics which is concerned merely with what is derivable as opposed to how it is derivable, paying attention to the fact that it is the how that determines the answer constraint. On the other side our approach is distinguished from so-called external logic characterizations of the operational semantics of logic programming. There, operational semantics are axiomatized in a classical meta-logic specifying the program behaviour in terms of successful and failing queries. Here, in contrast, QLL is used as an internal logic in which operational semantics are not differentiated by different axiom systems but by different rule systems. Or, to put it at another level: Formulas in QLL do not specify properties of programs but the programs themselves.
Technically, we first extend existing work on Propositional Lax Logic (PLL) to a first-order language (QLL), presenting a soundness and completeness theorem for a Gentzen-style system via a syntactic translation into a classical first-order bimodal theory. Previous work on applying Lax Logic to deal with behavioural constraints in formal hardware verification has demonstrated the complementary nature of abstraction and constraints; we proceed to show how the Lax Logic Programming (LLP) fragment of QLL can reveal abstractions behind Constraint Logic Programming (CLP). Our main tool is an intensional first-order extension of the Curry-Howard isomorphism between natural deduction proofs in PLL and terms of the computational lambda calculus. Instantiating the monadic operator of QLL by a generic notion of constraint computation, we factor a concrete CLP program into two parts: an abstract LLP program and an associated constraint table. These tables allow us to recover concrete answer constraints for CLP programs from abstract LLP derivations, and thus to establish precise proof- and model-theoretic connections between our Lax logical account of CLP and existing work. Choosing different notions of constraint allows us to generalize the standard notion of constraint (as in CLP) and to apply the LLP paradigm to the complementary problems of program abstraction and program refinement.