Answers Synthesis for CLP with Negation.
Gilles Richard, Frédéric Saubion · 1996
. Rewrite techniques can be used to execute logic programs in order to avoid some drawbacks of classical Prolog resolution. Logic programs are represented as rewrite programs whose operational mechanism, inspired from Knuth-Bendix completion, allows to prune some unnecessary computations and offers a synthesis ability which enables to represent infinite sets of answers as finite sets of formulas. We extend this approach to CLP with negation. Our mechanism, integrating both non symbolic constraints and negation, keeps the loop avoiding and synthesis properties. Taking advantage of a simplification rule, the solutions are obtained as a set of constrained rewrite rules with more expressive power than simple constraints used in classical CLP resolution. The system is proved sound and complete with regard to the standard CLP semantics. 1 INTRODUCTION Rewrite techniques, adapted to a pure logic programming framework by Bonacina and Hsiang in [3], provide a new evaluation mechanism for logic...