Abstract

Rewrite techniques can be used to execute logic programs in order to avoid some drawbacks of classical Prolog resolution. By transforming clauses into logical equivalences considered as rewrite rules, logic programs are represented as rewrite programs whose operational mechanism, inspired from the Knuth-Bendix completion, allows one to prune some unnecessary computations and offers a synthesis ability which enables to represent infinite sets of answers as finite sets of formulas. We propose here a full extension of this approach to Constraint Logic Programming with negation. Issued from rewrite techniques, a very powerful simplification rule is defined, available in a more general context than strict instantiation. Thanks to this rule, solutions are obtained as a set of constraint rewrite rules with more expressive power than simple constraints used in a classical CLP framework. Thus, our mechanism, integrating both non symbolic constraints and negation, keeps the loop avoiding and synthesis properties. Furthermore, the system is proved sound and complete with regard to the standard CLP semantics. There is an implementation of our mechanism : at this step, this is only a prototype written in Prolog