{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T22:25:13Z","timestamp":1750458313960},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2007,9,1]],"date-time":"2007-09-01T00:00:00Z","timestamp":1188604800000},"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":[[2007,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present in this paper a general algorithm for solving first-order formulas in particular theories called <jats:italic>decomposable theories<\/jats:italic>. First of all, using special quantifiers, we give a formal characterization of decomposable theories and show some of their properties. Then, we present a general algorithm for solving first-order formulas in any decomposable theory <jats:italic>T<\/jats:italic>. The algorithm is given in the form of five rewriting rules. It transforms a first-order formula \u03d5, which can possibly contain free variables, into a conjunction \u03c6 of solved formulas easily transformable into a Boolean combination of existentially quantified conjunctions of atomic formulas. In particular, if \u03d5 has no free variables then \u03c6 is either the formula <jats:italic>true<\/jats:italic> or \u00ac<jats:italic>true<\/jats:italic>. The correctness of our algorithm proves the completeness of the decomposable theories. Finally, we show that the theory <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S1471068406002997_inline1\"><jats:alt-text>${\\cal T}$<\/jats:alt-text><\/jats:inline-graphic> of finite or infinite trees is a decomposable theory and give some benchmarks realized by an implementation of our algorithm, solving formulas on two-partner games in <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S1471068406002997_inline1\"><jats:alt-text>${\\cal T}$<\/jats:alt-text><\/jats:inline-graphic> with more than 160 nested alternated quantifiers.<\/jats:p>","DOI":"10.1017\/s1471068406002997","type":"journal-article","created":{"date-parts":[[2007,8,24]],"date-time":"2007-08-24T10:55:18Z","timestamp":1187952918000},"page":"583-632","source":"Crossref","is-referenced-by-count":9,"title":["Decomposable theories"],"prefix":"10.1017","volume":"7","author":[{"given":"KHALIL","family":"DJELLOUL","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2007,9,1]]},"reference":[{"key":"S1471068406002997_ref32","unstructured":"Smith A. 1991. Constraint operations for CLP. Logic Programming: Proceedings of the 8th International Conference, Paris. pp. 760\u2013774."},{"key":"S1471068406002997_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"S1471068406002997_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57529-4_54"},{"key":"S1471068406002997_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/371316.371494"},{"key":"S1471068406002997_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/357162.357169"},{"key":"S1471068406002997_ref25","unstructured":"Maher M. 1988. Complete axiomatization of the algebra of finite, rational and infinite trees. Technical report, IBM T.J.Watson Research Center."},{"key":"S1471068406002997_ref24","unstructured":"Lyndon R. C. 1964. Notes on Logic. Van Nostrand Mathematical studies."},{"key":"S1471068406002997_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(87)90007-0"},{"key":"S1471068406002997_ref22","volume-title":"Introduction to Automata Theory, Languages and Computation.","author":"John","year":"1979"},{"key":"S1471068406002997_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037057"},{"key":"S1471068406002997_ref20","unstructured":"Huet G. 1976. Resolution d'equations dans les langages d'ordre 1, 2,.\u00a0.\u00a0.\u03c9. These d'Etat, Universite Paris 7. France."},{"key":"S1471068406002997_ref19","volume-title":"Essentials of Constraints Programming","author":"Fruehwirth","year":"2002"},{"key":"S1471068406002997_ref18","unstructured":"Djelloul K. and Dao T. 2006b. Complete first-order axiomatization of the M-extended trees. Proceeding of the 20th Workshop on (constraint) Logic Programming (WLP06). INFSYS Research Report 1843-06-02, pp. 111\u2013119."},{"key":"S1471068406002997_ref17","volume-title":"Proceeding of the 21st ACM Symposium on Applied Computing (SAC).","author":"Djelloul","year":"2006"},{"key":"S1471068406002997_ref16","first-page":"106","article-title":"About the combination of trees and rational numbers in a complete first-order theory","volume":"3717","author":"Djelloul","year":"2005","journal-title":"Proceeding of the 5th International conference on frontiers of combining systems FroCoS 2005"},{"key":"S1471068406002997_ref15","first-page":"87","volume-title":"Proceedings of the 2005 International Conference on Foundations of Computer Science (FCS'05)","author":"Djelloul","year":"2005"},{"key":"S1471068406002997_ref5","unstructured":"Colmerauer A. 1984. Equations and inequations on finite and infinite trees. Proceeding of the International Conference on the Fifth Generation of Computer Systems, pp. 85\u201399."},{"key":"S1471068406002997_ref6","first-page":"68","article-title":"An introduction to Prolog III","volume":"7","author":"Colmerauer","year":"1990","journal-title":"Comm. ACM, 33"},{"key":"S1471068406002997_ref33","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/3-540-61511-3_91","article-title":"An Improved Lower Bound for the Elementary Theories of Trees","volume":"1104","author":"Vorobyov","year":"1996","journal-title":"Proceeding of the 13th International Conference on Automated Deduction (CADE'96)"},{"key":"S1471068406002997_ref3","volume-title":"Negation as failure. In Logic and Data bases","author":"Clark","year":"1978"},{"key":"S1471068406002997_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90050-2"},{"key":"S1471068406002997_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90059-2"},{"key":"S1471068406002997_ref26","first-page":"262","volume-title":"The Metamathematics of Algebraic Systems","author":"Malcev","year":"1971"},{"key":"S1471068406002997_ref14","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":"S1471068406002997_ref7","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025675127871"},{"key":"S1471068406002997_ref8","unstructured":"Comon H. 1988. Unification et disunification: Theorie et applications. PhD thesis, Institut National Polytechnique de Grenoble."},{"key":"S1471068406002997_ref4","first-page":"231","volume-title":"Prolog and infinite trees","author":"Colmerauer","year":"1982"},{"key":"S1471068406002997_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90043-0"},{"key":"S1471068406002997_ref1","volume-title":"Le manuel de Prolog IV. PrologIA","author":"Benhamou","year":"1996"},{"key":"S1471068406002997_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012853"},{"key":"S1471068406002997_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80017-3"},{"key":"S1471068406002997_ref10","volume-title":"Computational Logic: Essays in Honor of Alan Robinson.","author":"Comon","year":"1991"},{"key":"S1471068406002997_ref11","unstructured":"Comon H. 1991. Resolution de contraintes dans des algebres de termes. Rapport d'Habilitation, Universite de Paris Sud."}],"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\/S1471068406002997","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,29]],"date-time":"2019-03-29T19:10:34Z","timestamp":1553886634000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068406002997\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,9]]},"references-count":33,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2007,9]]}},"alternative-id":["S1471068406002997"],"URL":"https:\/\/doi.org\/10.1017\/s1471068406002997","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,9]]}}}