Solving first-order constraints in the theory of finite or infinite trees: introduction to the decomposable theories

ABSTRACT

We present in this paper an algorithm in the theory T of possibly infinite trees for solving general constraints represented by full first-order formulas, with equality as the only relation and functional symbols taken from an infinite set F. The algorithm consists of a set of 11 rewriting rules. It transforms a first-order formula p in a conjunction q of solved formulas, equivalent in T, such that: (1) the conjunction q is the formula true if p is always true in T, and the formula ¬true if p is always false in T. Moreeover, if p or its negation has a finite base of solutions in a model of T, then these solutions or non-solutions have to be explicit in q. (2) each solved formula of q has not new free variables and can be transformed immediately in a Boolean combination of basic formulas whose length does not exceed twice the length of the solved formula. The basic formulas are particular cases of existentially quantified conjunctions of equations. The correctness of the algorithm gives another proof of the completeness of T demonstrated by Michael Maher. We test our algorithm on benchmarks realized by an implementation, solving formulas on two-partners games in T with more than 160 nested alternated quantifiers.Finally, we show then that we can generalize this algorithm by introducing a new class of theories that we call decomposable. We show that T is decomposable and give a general algorithm for solving first-order constraint in any decomposable theory. The correctness of our algorithm shows the completeness of the decomposable theories.

REFERENCES

• 1: Benhamou F, Colmerauer, Van caneghem M. Le manuel de Prolog IV, PrologIA, Marseille, France, 1996.
• 2: Hans-Jürgen Bürckert, Solving Disequations in Equational Theories, Proceedings of the 9th International Conference on Automated Deduction, p.517-526, May 23-26, 1988
• 3: 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]
• 4: Colmerauer A. Equations and inequations on finite and infinite trees. Proceeding of the International conference on the fifth generation of computer systems Tokyo, 1984. P. 85--99.
• 5: Hubert Comon , Pierre Lescanne, Equational problems and disunification, Journal of Symbolic Computation, v.7 n.3-4, p.371-425, March/April 1989 [doi>10.1016/S0747-7171(89)80017-3]
• 6: Comon H. Unification et disunification: Thorie et applications. PhD thesis, Institut National Polytechnique de Grenoble, 1988.
• 7: Comon H. Disunification: a survey. In J. L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991.
• 8: Comon H. Rsolution de contraintes dans des algbres de termes. Rapport d'Habilitation, Universit de Paris Sud, 1991.
• 9: Courcelle B. Equivalences and Transformations of Regular Systems applications to Program Schemes and Grammars, Theretical Computer Science, vol. 42, 1986, p. 1--122.
• 10: 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]
• 11: Dao H. Rsolution de contraintes du premier ordre dans la thorie des arbres finis ou infinis. Thse d'informatique, Universit de la mditerrane, dcembre 2000.
• 12: Djelloul K. Complete first-order axiomatisation of the construction of trees on an ordered set. Proceedings of the 2005 International Conference on Foundations of Computer Science (FCS'05) Las Vegas, CSREA Press.
• 13: Djelloul K. About the combination of trees and rational numbers in a complete first-order theory. Proceeding of the 5th International conference on frontiers of combining systems FroCoS 2005, Vienna Austria. LNAI, vol 3717, P. 106--122.
• 14: Huet G. Resolution d'equations dans les langages d'ordre 1, 2,.. ω. These d'Etat, Universite Paris 7. France, 1976.
• 15: Jaffar J. Efficient unification over infinite terms. New Generation Computing, 2(3): P. 207--219, 1984.
• 16: John E. and Ullman D. Introduction to automata theory, languages and computation. Addison-Wesley publishing company, 1979.
• 17: Kenneth Kunen, Negation in logic programming, Journal of Logic Programming, v.4 n.4, p.289-308, December 1, 1987 [doi>10.1016/0743-1066(87)90007-0 ]
• 18: Maher M. Complete axiomatization of the algebra of finite, rational and infinite trees. Technical report, IBM, 1988.
• 19: Alberto Martelli , Ugo Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.2, p.258-282, April 1982 [doi>10.1145/357162.357169]
• 20: Paterson M and Wegman N. Linear unification. Journal of Computer and Systems Science, 16:158167, 1978.
• 21: Viswanath Ramachandran , Pascal Van Hentenryck, Incremental Algorithms for Constraint Solving and Entailment over Rational Trees, Proceedings of the 13th Conference on Foundations of Software Technology and Theoretical Computer Science, p.205-217, December 15-17, 1993
• 22: 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]
• 23: Sergei G. Vorobyov, An Improved Lower Bound for the Elementary Theories of Trees, Proceedings of the 13th International Conference on Automated Deduction: Automated Deduction, p.275-287, August 03, 1996

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

General Terms:
Algorithms, Theory

Keywords:
complete theory, first-order constraints, rewriting rules, theory of trees, two partners games