Modelling PROLOG Control in Constraint Logic Languages

We define a "logical denotational semantics" for pure PROLOG programs, and prove it correct and complete wrt an operational one. Our semantics is given as an instance of a generalized semantics for CLP and is naturally oriented towards abstract interpretation. The key feature is that prolog control strategy is modeled inside the constraint system, mantaining the logical flavor of classical semantics for pure logic programming. 1 Introduction An elegant and promising technique for analyzing logic programs is that based on constraints, first introduced in [3] and then formalized in terms of the so-called generalized semantics in [6, 7, 5]. The extension of logic programming ([15]) that replaces the usual unification on the Herbrand universe with a more general notion of constraint is called constraint logic programming (CLP, [8]). The semantics of CLP is usually given in terms of algebraic structures, called constraint systems (CS, [8, 13]). We follow here the approach of [8], which defi..