Hostname: page-component-586b7cd67f-l7hp2 Total loading time: 0 Render date: 2024-11-25T08:12:10.496Z Has data issue: false hasContentIssue false
  • English
  • Français

Theory of finite or infinite trees revisited

Published online by Cambridge University Press:  12 May 2008

KHALIL DJELLOUL ,
THI-BICH-HANH DAO  and
THOM FRÜHWIRTH
KHALIL DJELLOUL
Affiliation:
Faculty of computer science, University of Ulm, Germany
THI-BICH-HANH DAO
Affiliation:
Laboratoire d'informatique fondamentale d'Orleans, Universite d'Orleans, France
THOM FRÜHWIRTH
Affiliation:
Faculty of computer science, University of Ulm, Germany
Get access Rights & Permissions [Opens in a new window]

Abstract

We present in this paper a first-order axiomatization of an extended theory T of finite or infinite trees, built on a signature containing an infinite set of function symbols and a relation finite(t), which enables to distinguish between finite and infinite trees. We show that T has at least one model and prove its completeness by giving not only a decision procedure, but a full first-order constraint solver that gives clear and explicit solutions for any first-order constraint satisfaction problem in T. The solver is given in the form of 16 rewriting rules that transform any first-order constraint ϕ into an equivalent disjunction φ of simple formulas such that φ is either the formula true or the formula false or a formula having at least one free variable, being equivalent neither to true nor to false and where the solutions of the free variables are expressed in a clear and explicit way. The correctness of our rules implies the completeness of T. We also describe an implementation of our algorithm in CHR (Constraint Handling Rules) and compare the performance with an implementation in C++ and that of a recent decision procedure for decomposable theories.

Keywords

logical first-order formulatheory of finite or infinite treescomplete theoryrewriting rules
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 8 , Issue 4 , July 2008 , pp. 431 - 489
Copyright
Copyright © Cambridge University Press 2008

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

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.CrossRefGoogle Scholar
Baader, F. and Nipkow, T. 1998. Term Rewriting and All That. Cambridge University Press. ISBN 0-521-45520–0.CrossRefGoogle Scholar
Benhamou, F., Colmerauer, A., Garetta, H., Pasero, R. and Van-caneghem, M. 1996. Le manuel de Prolog IV. PrologIA, Marseille, France.Google Scholar
Burckert, H. 1988. Solving disequations in equational theories. In Proceeding of the 9th Conference on Automated Deduction, LNCS 310. Springer-Verlag, 517–526.Google Scholar
Clark, K. L. 1978. Negation as failure. In Logic and Data Bases. Gallaire, H., and Minker, J., Eds. Plenum Pub.Google Scholar
Colmerauer, A. 1982. Prolog and infinite trees. In Logic Programming, Clark, K. L. and Tarnlund, S.-A., Ed. Academic Press, 231–251.Google Scholar
Colmerauer, A., Kanoui, H. and Van-caneghem, M. 1983. Prolog, theoretical basis and current developments. TSI (Technology and Science of Informatics) 2 (4), 271–311.Google Scholar
Colmerauer, A. 1984. Equations and inequations on finite and infinite trees. In Proceedings of the International Conference on the Fifth Generation of Computer Systems, 85–99.Google Scholar
Colmerauer, A. 1990. An introduction to Prolog III. Communication of the ACM 33 (7), 68–90.CrossRefGoogle Scholar
Colmerauer, A. and Dao, T. 2003. Expressiveness of full first-order formulas in the algebra of finite or infinite trees. Constraints 8 (3), 283–302.CrossRefGoogle Scholar
Comon, H. 1988. Unification et disunification : Theorie et applications. PhD thesis, Institut National Polytechnique de Grenoble.Google Scholar
Comon, H. and Lescanne, P. 1989. Equational problems and disunification. Journal of Symbolic Computation 7, 371–425.CrossRefGoogle Scholar
Comon, H. 1991a. Disunification: a survey. In Computational Logic: Essays in Honor of Alan Robinson, Lassez, J. L. and Plotkin, G., Ed. MIT Press.Google Scholar
Comon, H. 1991b. Resolution de contraintes dans des algebres de termes. Rapport d'Habilitation, Universite de Paris Sud.Google Scholar
Courcelle, B. 1983. Fundamental properties of infinite trees. Theoretical Computer Science 25 (2), 95–169.CrossRefGoogle Scholar
Courcelle, B. 1986. Equivalences and transformations of regular systems applications to program schemes and grammars. Theoretical Computer Science 42, 100–122.CrossRefGoogle Scholar
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.Google Scholar
Djelloul, K. 2006a. Decomposable theories. Journal of Theory and Practice of Logic Programming (to appear).CrossRefGoogle Scholar
Djelloul, K. and Dao, T. 2006b. Solving first-order formulas in the theory of finite or infinite trees : Introduction to the decomposable theories. In Proceeding of the 21st ACM Symposium on Applied Computing (SAC'06). ACM Press, 7–14.Google Scholar
Duck, G., Stuckey, P., Banda, M. and Holzbaur, C. 2004. The refined operational semantics of constraint handling rules. In Proceedings of the 20th International Conference on Logic Programming. LNCS 3132, 105–119.Google Scholar
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.CrossRefGoogle Scholar
Fruehwirth, T. and Abdennadher, S. 2003. Essentials of Constraint Programming. Springer.CrossRefGoogle Scholar
Fruehwirth, T. 2005. Parallelizing union-find in constraint handling rules using confluence. In Proceedings of the 21st International Conference of Logic Programming. LNCS, Vol 3668, 113–127.Google Scholar
Herbrand, J. 1930. Recherches sur la theorie de la demonstration. PhD thesis, Universite de Paris, France.Google Scholar
Huet, G. 1976. Resolution d'equations dans les langages d'ordre 1, 2, . . .ω. These d'Etat, Universite Paris 7. France.Google Scholar
Jaffar, J. 1984. Efficient unification over infinite terms. New Generation Computing 2 (3), 207–219.CrossRefGoogle Scholar
John, E. and Ullman, D. 1979. Introduction to Automata Theory, Languages and Computation. Addison-Wesley publishing company.Google Scholar
Jouannaud, J. P. and Kirchner, C. 1991. Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification. Computational Logic – Essays in Honor of Alan Robinson. MIT Press, 257–321.Google Scholar
Kunen, K. 1987. Negation in logic programming. Journal of Logic Programming 4, 289–308.CrossRefGoogle Scholar
Lassez, J., Maher, M. and Marriott, K. 1986. Unification revisited. In Proceedings of the Workshop on the Foundations of Deductive Database and Logic Programming, 587–625.Google Scholar
Lassez, J. and Marriott, K. 1987. Explicit representation of terms defined by counter examples. Journal of Automated Reasonning 3, 301–317.Google Scholar
Lassez, J. and McAloon, K. 1989. Independence of negative constraints. In Proceedings of TOPSOFT, LNCS 351, 19–27.Google Scholar
Lyndon, R. C. 1964. Notes on Logic. Van Nostrand Mathematical studies.Google Scholar
Maher, M. 1988. Complete Axiomatization of the Algebra of Finite, Rational and Infinite Trees. Technical report, IBM – T. J. Watson Research Center.CrossRefGoogle Scholar
Maher, M. and Stuckey, P. 1995. On inductive inference of cyclic structures. Annals of Mathematics and Artificial Intelligence 15 (2), 167–208.CrossRefGoogle Scholar
Malcev, A. 1971. Axiomatizable classes of locally free algebras of various types. In The Metamathematics of Algebraic Systems Wells, B. III, Ed. Anatolii Ivanovic Malcev. Collected Papers: 1936–1967, vol. 66, chapter 23, pp. 262–281.Google Scholar
Martelli, A. and Montanari, U. 1982. An efficient unification algorithm. ACM Trans. on Languages and Systems 4 (2), 258–282.CrossRefGoogle Scholar
Meister, M. and Fruehwirth, T. 2006. Complexity of the CHR rational tree equation solver. In Proceedings of the Third Workshop on Constraint Handling Rules.Google Scholar
Paterson, M. and Wegman, N. 1978. Linear unification. Journal of Computer and Systems Science 16, 158–167.CrossRefGoogle Scholar
Podelski, A. and Van Roy, P. 1994. The beauty and beast algorithm: quasi-linear incremental tests of entailment and disentailment over trees. In Proceedings of the 1994 International Symposium on Logic Programming. MIT Press, 359–374.Google Scholar
Ramachandran, V. and Van Hentenryck, P. 1993. Incremental algorithms for formula solving and entailment over rational trees. In Proceedings of the 13th Conference Foundations of Software Technology and Theoretical Computer Science, LNCS volume 761, 205–217.Google Scholar
Robinson, J. A. 1965. A machine-oriented logic based on the resolution principle. JACM, 12 (1), 23–41.CrossRefGoogle Scholar
Rybina, T. and Voronkov, A. 2001. A decision procedure for term algebras with queues. ACM Transaction on Computational Logic 2 (2), 155–181.Google Scholar
Schrijvers, T., Demoen, B., Duck, G., Stuckey, P. and Fruehwirth, T. 2006. Automatic implication checking for CHR constraints. In Proceedings of the 6th International Workshop on Rule-Based Programming. ENTC, vol 147, pp. 93–111.Google Scholar
Schrijvers, T. and Fruehwirth, . CHR Website, www.cs.kuleuven.ac.be/~dtai/projects/CHR/Google Scholar
Smith, A. 1991. Constraint operations for CLP. In Logic Programming: Proceedings of the 8th International Conference, Paris, 760–774.Google Scholar
Van Weert, P., Sneyers, J., Schrijvers, T. and Demoen, B. 2006. Constraint handling rules with negations as absence. In Proceedings of the Third Workshop on Constraint Handling Rules.CrossRefGoogle Scholar
Vorobyov, S. 1996. An improved lower bound for the elementary theories of trees, In Proceeding of the 13th International Conference on Automated Deduction (CADE'96). Springer Lecture Notes in Artificial Intelligence, vol. 1104, pp. 275–287.Google Scholar