Master's Thesis
Cesare Tinelli,
Extending the CLP Scheme to Unions of Constraint Theories,
Department of Computer Science,
University of Illinois at Urbana-Champaign,
October 1995.
Advisor
Mehdi Harandi
Abstract
The Constraint Logic Programming scheme extends conventional Logic Programming by replacing the notion of unifiability with that of constraint solvability over an underlying constraint domain or theory.
As originally proposed, the CLP scheme extends immediately to the case of multiple constraint theories as long as their signatures do not share function or predicate symbols.
The scheme though does not account for the presence of mixed terms, that is, terms built with functors from different signatures, and corresponding mixed constraints.
As a matter of fact, current multi-domain CLP systems do not allow mixed terms or restrict them considerably by accepting terms like f(X+1) , for instance, and refusing as ill-typed or undefined terms like f(X)+1 .
The reason for this is that, although the CLP scheme allows in principle multiple, separate constraint theories, each with its own constraint solver, it is not designed to operate on their union , to which mixed terms and constraints belong.
In this thesis, we propose an extension of the CLP scheme that operates with unions of constraint theories and decides the satisfiability of mixed constraints by appropriately combining the constraint solvers of the single 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.
Finally, we discuss briefly some implementation issues and give directions for further developments.
[A comprehensive description of the work above has been published in the
The
Journal of Functional Logic Programming
with the title Constraint Logic Programming over Unions of Constraint Theories.]
Last Updated: October 1999
