Logic Program Schemas, Semi-Unification and Constraints

The use of schemas is a classical way of synthesizing, transforming and analyzing logic programs. Operations on schemas are needed, in particular, the semi-unification of schemas with programs. Since schemas are second-order objects, the related semi-unification is the second-order semi-unification, which is decidable but NP-complete. The non-determinism implied by the NP-completeness slows down the search for a substitution. The present paper expresses the semi-unification process over schemas as rewriting and reduction rules. Global and local constraints are associated to the schema to extend the expressivity of schema description and to fasten the search for a second-order substitution between programs and schemas. CLP techniques and notations are used. 1 Introduction In logic programming, the use of program schemas is a very promising technique. In program synthesis, program schemas can formalize particular resolution methods (divide-and-conquer, generate-and-test approaches...),..