Constraint Logic Programming over Unions of Constraint Theories.
Cesare Tinelli, Mehdi T. Harandi · 1998
. In this paper, we propose an extension of the Jaffar-Lassez Constraint Logic Programming scheme that operates with unions of constraint theories with different signatures and decides the satisfiability of mixed constraints by appropriately combining the constraint solvers of the component theories. We describe the extended scheme and provide logical and operational semantics for it along the lines of those given for the original scheme. Then we show how the main soundness and completeness results of Constraint Logic Programming lift to our extension. Keywords: Constraint Logic Programming, combination of satisfiability procedures. 1 Introduction The Constraint Logic Programming scheme was originally developed in [8] by Jaffar and Lassez as a principled way to combine the two computational paradigms of Logic Programming and Constraint Solving. The scheme extends conventional Logic Programming by replacing the notion of unifiability with that of constraint solvability over an underl...