{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T06:16:30Z","timestamp":1784873790228,"version":"3.55.0"},"reference-count":48,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2008,5,12]],"date-time":"2008-05-12T00:00:00Z","timestamp":1210550400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2008,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n\t  <jats:p>We present in this paper a first-order axiomatization of an extended theory <jats:italic>T<\/jats:italic> of finite or infinite trees, built on a signature containing an infinite set of function symbols and a relation <jats:italic>finite<\/jats:italic>(<jats:italic>t<\/jats:italic>), which enables to distinguish between finite and infinite trees. We show that <jats:italic>T<\/jats:italic> 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 <jats:italic>T<\/jats:italic>. The solver is given in the form of 16 rewriting rules that transform any first-order constraint \u03d5 into an equivalent disjunction \u03c6 of simple formulas such that \u03c6 is either the formula <jats:italic>true<\/jats:italic> or the formula <jats:italic>false<\/jats:italic> or a formula having at least one free variable, being equivalent neither to <jats:italic>true<\/jats:italic> nor to <jats:italic>false<\/jats:italic> 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 <jats:italic>T<\/jats:italic>. 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.<\/jats:p>","DOI":"10.1017\/s1471068407003171","type":"journal-article","created":{"date-parts":[[2008,5,12]],"date-time":"2008-05-12T14:12:39Z","timestamp":1210601559000},"page":"431-489","source":"Crossref","is-referenced-by-count":13,"title":["Theory of finite or infinite trees revisited"],"prefix":"10.1017","volume":"8","author":[{"given":"KHALIL","family":"DJELLOUL","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"THI-BICH-HANH","family":"DAO","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"THOM","family":"FR\u00dcHWIRTH","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2008,5,12]]},"reference":[{"key":"S1471068407003171_manual_ref-25","volume-title":"Resolution d'equations dans les langages d'ordre 1, 2,\u00a0.\u00a0.\u00a0.\u03c9","author":"Huet","year":"1976"},{"key":"S1471068407003171_manual_ref-26","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037057"},{"key":"S1471068407003171_manual_ref-22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-05138-2"},{"key":"S1471068407003171_manual_ref-37","doi-asserted-by":"publisher","DOI":"10.1145\/357162.357169"},{"key":"S1471068407003171_manual_ref-35","doi-asserted-by":"publisher","DOI":"10.1007\/BF01534454"},{"key":"S1471068407003171_manual_ref-5","volume-title":"Logic and Data Bases","author":"Clark","year":"1978"},{"key":"S1471068407003171_manual_ref-46","unstructured":"Smith, A. 1991. Constraint operations for CLP. In Logic Programming: Proceedings of the 8th International Conference, Paris, 760\u2013774."},{"key":"S1471068407003171_manual_ref-17","unstructured":"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."},{"key":"S1471068407003171_manual_ref-14","unstructured":"Comon, H. 1991b. Resolution de contraintes dans des algebres de termes. Rapport d'Habilitation, Universite de Paris Sud."},{"key":"S1471068407003171_manual_ref-13","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"Comon","year":"1991"},{"key":"S1471068407003171_manual_ref-30","doi-asserted-by":"crossref","unstructured":"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\u2013625.","DOI":"10.1016\/B978-0-934613-40-8.50019-1"},{"key":"S1471068407003171_manual_ref-36","doi-asserted-by":"crossref","unstructured":"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\u20131967, vol. 66, chapter 23, pp. 262\u2013281.","DOI":"10.1016\/S0049-237X(08)70560-3"},{"key":"S1471068407003171_manual_ref-33","volume-title":"Notes on Logic","author":"Lyndon","year":"1964"},{"key":"S1471068407003171_manual_ref-21","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10005-5"},{"key":"S1471068407003171_manual_ref-23","doi-asserted-by":"crossref","unstructured":"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\u2013127.","DOI":"10.1007\/11562931_11"},{"key":"S1471068407003171_manual_ref-24","unstructured":"Herbrand, J. 1930. Recherches sur la theorie de la demonstration. PhD thesis, Universite de Paris, France."},{"key":"S1471068407003171_manual_ref-3","unstructured":"Benhamou, F. , Colmerauer, A. , Garetta, H. , Pasero, R. and Van-caneghem, M. 1996. Le manuel de Prolog IV. PrologIA, Marseille, France."},{"key":"S1471068407003171_manual_ref-10","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025675127871"},{"key":"S1471068407003171_manual_ref-8","unstructured":"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\u201399."},{"key":"S1471068407003171_manual_ref-19","doi-asserted-by":"crossref","unstructured":"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\u201314.","DOI":"10.1145\/1141277.1141280"},{"key":"S1471068407003171_manual_ref-28","first-page":"257","volume-title":"Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification","author":"Jouannaud","year":"1991"},{"key":"S1471068407003171_manual_ref-6","unstructured":"Colmerauer, A. 1982. Prolog and infinite trees. In Logic Programming, Clark, K. L. and Tarnlund, S.-A. , Ed. Academic Press, 231\u2013251."},{"key":"S1471068407003171_manual_ref-9","doi-asserted-by":"publisher","DOI":"10.1145\/79204.79210"},{"key":"S1471068407003171_manual_ref-4","doi-asserted-by":"crossref","unstructured":"Burckert, H. 1988. Solving disequations in equational theories. In Proceeding of the 9th Conference on Automated Deduction, LNCS 310. Springer-Verlag, 517\u2013526.","DOI":"10.1007\/BFb0012853"},{"key":"S1471068407003171_manual_ref-38","unstructured":"Meister, M. and Fruehwirth, T. 2006. Complexity of the CHR rational tree equation solver. In Proceedings of the Third Workshop on Constraint Handling Rules."},{"key":"S1471068407003171_manual_ref-39","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90043-0"},{"key":"S1471068407003171_manual_ref-43","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1145\/371316.371494","article-title":"A decision procedure for term algebras with queues","volume":"2","author":"Rybina","year":"2001","journal-title":"ACM Transaction on Computational Logic"},{"key":"S1471068407003171_manual_ref-2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"},{"key":"S1471068407003171_manual_ref-16","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90050-2"},{"key":"S1471068407003171_manual_ref-1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0017444"},{"key":"S1471068407003171_manual_ref-12","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80017-3"},{"key":"S1471068407003171_manual_ref-29","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(87)90007-0"},{"key":"S1471068407003171_manual_ref-27","volume-title":"Introduction to Automata Theory, Languages and Computation","author":"John","year":"1979"},{"key":"S1471068407003171_manual_ref-32","doi-asserted-by":"crossref","unstructured":"Lassez, J. and McAloon, K. 1989. Independence of negative constraints. In Proceedings of TOPSOFT, LNCS 351, 19\u201327.","DOI":"10.1007\/3-540-50939-9_122"},{"key":"S1471068407003171_manual_ref-34","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5132"},{"key":"S1471068407003171_manual_ref-41","doi-asserted-by":"crossref","unstructured":"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\u2013217.","DOI":"10.1007\/3-540-57529-4_54"},{"key":"S1471068407003171_manual_ref-7","first-page":"271","article-title":"Prolog, theoretical basis and current developments","volume":"2","author":"Colmerauer","year":"1983","journal-title":"TSI (Technology and Science of Informatics)"},{"key":"S1471068407003171_manual_ref-18","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068406002997"},{"key":"S1471068407003171_manual_ref-20","doi-asserted-by":"crossref","unstructured":"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\u2013119.","DOI":"10.1007\/978-3-540-27775-0_7"},{"key":"S1471068407003171_manual_ref-40","unstructured":"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\u2013374."},{"key":"S1471068407003171_manual_ref-44","doi-asserted-by":"crossref","unstructured":"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\u2013111.","DOI":"10.1016\/j.entcs.2005.06.039"},{"key":"S1471068407003171_manual_ref-48","doi-asserted-by":"crossref","unstructured":"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\u2013287.","DOI":"10.1007\/3-540-61511-3_91"},{"key":"S1471068407003171_manual_ref-11","unstructured":"Comon, H. 1988. Unification et disunification : Theorie et applications. PhD thesis, Institut National Polytechnique de Grenoble."},{"key":"S1471068407003171_manual_ref-15","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90059-2"},{"key":"S1471068407003171_manual_ref-45","unstructured":"Schrijvers, T. and Fruehwirth, . CHR Website, www.cs.kuleuven.ac.be\/~dtai\/projects\/CHR\/"},{"key":"S1471068407003171_manual_ref-47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74610-2_39"},{"key":"S1471068407003171_manual_ref-31","first-page":"301","article-title":"Explicit representation of terms defined by counter examples","volume":"3","author":"Lassez","year":"1987","journal-title":"Journal of Automated Reasonning"},{"key":"S1471068407003171_manual_ref-42","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068407003171","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T22:09:54Z","timestamp":1750457394000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068407003171\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,5,12]]},"references-count":48,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["S1471068407003171"],"URL":"https:\/\/doi.org\/10.1017\/s1471068407003171","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,5,12]]}}}