Toward a first-order extension of Prolog's unification using CHR: a CHR first-order constraint solver over finite or infinite trees

ABSTRACT

Prolog, which stands for PROgramming in LOGic, is the most widely used language in the logic programming paradigm. One of its main concepts is unification. It represents the mechanism of binding the contents of variables and can be seen as solving conjunctions of equations over finite or infinite trees. We present in this paper an idea of a first-order extension of Prolog's unification by giving a general algorithm for solving any first-order constraint in the theory T of finite or infinite trees, extended by a relation which allows to distinguish between finite and infinite trees. The algorithm is given in the form of 16 rewriting rules which transform any first-order formula φ into an equivalent disjunction ϕ of simple formulas in which the solutions of the free variables are expressed in a clear and explicit way. We end this paper describing a CHR implementation of our algorithm. CHR (Constraint Handling Rules) has originally been developed for writing constraint solvers, but the constraints here go much beyond implicitly quantified conjunctions of atomic constraints and are considered as arbitrary first-order formulas built on the signature of T. We discuss how we implement nested local constraint stores and what programming patterns and language features we found useful in the CHR implementation of our algorithm.

REFERENCES

• 1: Abdennadher, S. 1997. Operational Semantics and Confluence of Constraint Propagation Rules. In Proc of the third International Conference on Principles and Practice of Constraint Programming. LNCS 1330.
• 2: Benhamou, F., Colmerauer, A., Garetta, H., Pasero, R. and Van-caneghem, M. 1996. Le manuel de Prolog IV. PrologIA, Marseille, France.
• 3: Colmerauer, A. 1982. Prolog and infinite trees. In K. L. Clark and S-A. Tarnlund, editors, Logic Programming. Academic Press. pp. 231--251.
• 4: Colmerauer, A., Kanoui, H. and Van-caneghem, M. 1983. Prolog, Theoretical Basis and Current Developments. TSI 2(4):271--311.
• 5: Colmerauer, A. 1984. Equations and in equations on finite and infinite trees. Proceeding of the International conference on the fifth generation of computer systems, pp. 85--99.
• 6: Alain Colmerauer, An introduction to Prolog III, Communications of the ACM, v.33 n.7, p.69-90, July 1990 [doi>10.1145/79204.79210]
• 7: Alain Colmerauer , Thi-Bich-Hanh Dao, Expressiveness of Full First-Order Constraints in the Algebra of Finite or Infinite Trees, Constraints, v.8 n.3, p.283-302, July 2003 [doi>10.1023/A:1025675127871]
• 8: Dao, T. 2000. Resolution de contraintes du premier ordre dans la theorie des arbres finis ou infinis. These d'informatique, Universite de la mediterranee, France.
• 9: Djelloul, K. 2006. Decomposable theories. Journal of Theory and practice of logic programming TPLP. (to appear)
• 10: Duck, G., Stuckey, P., Banda, M. and Holzbaur, C. 2004. The Refined Operational Semantics of Constraint Handling Rules. In Proc of the 20th International Conference on Logic Programming. LNCS 3132, pp. 105--119.
• 11: Fruehwirth, T. 1998. Theory and Practice of Constraint Handling Rules. Special Issue on Constraint Logic Programming. Journal of Logic Programming. 37(1--3): 95--138.
• 12: Thom Fruewirth , Slim Abdennadher, Essentials of Constraint Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 2003
• 13: Fruehwirth, T. 2005. Parallelizing Union-Find in Constraint Handling Rules Using Confluence. In proc of the 21st International Conference of Logic Programming. LNCS, Vol 3668. pp: 113--127.
• 14: Maher M. Complete axiomatization of the algebra of finite, rational and infinite trees. Technical report, IBM, 1988.
• 15: Meister, M. and Fruehwirth, T. 2006. Complexity of the CHR Rational Tree Equation Solver. In Proc of the third Workshop on Constraint Handling Rules.
• 16: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 17: Roussel, F. 1975. Prolog : Manuel de Reference et d'Utilisation, Groupe d'Intelligence Artificielle, Marseille-Luminy.
• 18: Van Weert, P., Sneyers, J., Schrijvers, T. and Demoen, B. 2006. Constraint Handling Rules with Negations as Absence. In Proc of the third Workshop on Constraint Handling Rules.
• 19: Schrijvers, T., Demoen, B., Duck, G., Stuckey, P. and Fruehwirth, T. 2006. Automatic implication checking for CHR constraints. In Proc of the 6th International Workshop on Rule-Based Programming. ENTC, vol 147, pp. 93--111.
• 20: Schrijvers, T. and Fruehwirth. CHR Website, www.cs.kuleuven.ac.be/dtai/projects/CHR/

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Logic programming; Deduction (e.g., natural, rule-based)

General Terms:
Algorithms, Theory

Keywords:
CHR (Constraint Handling Rules), Prolog, first-order constraints solving, theory of finite or infinite trees, unification