THE SEMANTICS OF CONSTRAINT LOGIC PROGRAMS

The Constraint Logic Programming (CLP) Scheme was introduced by Jaffar and Lassez. The scheme gave a formal framework, based on constraints, for the basic operational, logical and algebraic semantics of an exte nded class of logic programs. This paper presents for the first time t he semantic foundations of CLP in a self-contained and complete packag e. The main contributions are threefold, First, we extend the original conference paper by presenting definitions and basic semantic constru cts from first principles, giving new and complete proofs for the main lemmas. Importantly, we clarify which theorems depend on conditions s uch as solution compactness, satisfaction completeness and independenc e of constraints. Second, we generalize the original results to allow for incompleteness of the constraint solver. This is important since a lmost all CLP systems use an incomplete solver. Third, we give conditi ons on the (possibly incomplete) solver which ensure that the operatio nal semantics is confluent, that is, has independence of literal sched uling. (C) 1998 Elsevier Science Inc. All rights reserved.