{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:40:07Z","timestamp":1747593607353,"version":"3.40.5"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031634970"},{"type":"electronic","value":"9783031634987"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":182,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We analyze the theory of rational trees with finitely many constructors, infinitely many atoms and an atomicity predicate. We design a new decision procedure, proving in addition that this theory is model-complete. We also show that the enrichment of the language with selectors and simultaneous parametric fixpoints enjoys quantifier elimination.<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_16","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"265-283","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Model Completeness for\u00a0Rational Trees"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6449-6883","authenticated-orcid":false,"given":"Silvio","family":"Ghilardi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0003-7769-328X","authenticated-orcid":false,"given":"Lia M.","family":"Poidomani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,1]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Bockmayr, A., Weispfenning, V.: Solving numerical constraints. In: Handbook of Automated Reasoning, vol.\u00a0II, pp. 751\u2013844. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50014-X"},{"key":"16_CR2","volume-title":"Model Theory","author":"C-C Chang","year":"1990","unstructured":"Chang, C.-C., Keisler, J.H.: Model Theory, 3rd edn. North-Holland Publishing Co., Amsterdam-London (1990)","edition":"3"},{"key":"16_CR3","unstructured":"Colmerauer, A.: Equations and inequations on finite and infinite trees. In: Fifth Generation Computer Systems (1984)"},{"issue":"4","key":"16_CR4","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1017\/S1471068407003171","volume":"8","author":"K Djelloul","year":"2008","unstructured":"Djelloul, K., Dao, T., Fr\u00fchwirth, T.W.: Theory of finite or infinite trees revisited. Theory Pract. Logic Program. 8(4), 431\u2013489 (2008)","journal-title":"Theory Pract. Logic Program."},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/3-540-44585-4_8","volume-title":"Computer Aided Verification","author":"A Dovier","year":"2001","unstructured":"Dovier, A., Piazza, C., Policriti, A.: A fast bisimulation algorithm. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 79\u201390. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_8"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/3-540-46002-0_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Gentilini","year":"2002","unstructured":"Gentilini, R., Piazza, C., Policriti, A.: Simulation as coarsest partition problem. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 415\u2013430. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_29"},{"key":"16_CR7","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1023\/A:1027328830731","volume":"31","author":"R Gentilini","year":"2003","unstructured":"Gentilini, R., Piazza, C., Policriti, A.: From bisimulation to simulation: coarsest partition problems. J. Autom. Reason. 31, 73\u2013103 (2003)","journal-title":"J. Autom. Reason."},{"key":"16_CR8","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/BF03037057","volume":"2","author":"J Jaffar","year":"1984","unstructured":"Jaffar, J.: Efficient unification over infinite terms. N. Gener. Comput. 2, 207\u2013219 (1984)","journal-title":"N. Gener. Comput."},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-62950-5_59","volume-title":"Rewriting Techniques and Applications","author":"D Kapur","year":"1997","unstructured":"Kapur, D.: Shostak\u2019s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 23\u201337. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-62950-5_59"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: Young, M., Devanbu, P.T. (eds.) Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2006, Portland, Oregon, USA, 5\u201311 November 2006, pp. 105\u2013116. ACM (2006)","DOI":"10.1145\/1181775.1181789"},{"key":"16_CR11","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1016\/0743-1066(87)90007-0","volume":"4","author":"K Kunen","year":"1987","unstructured":"Kunen, K.: Negation in logic programming. J. Logic Program. 4, 289\u2013308 (1987)","journal-title":"J. Logic Program."},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite trees. In: Proceedings Third Annual Symposium on Logic in Computer Science, pp. 348\u2013349. IEEE Computer Society (1988)","DOI":"10.1109\/LICS.1988.5132"},{"key":"16_CR13","unstructured":"Mal\u2019cev, A.: On the elementary theory of locally free algebras. Soviet Math. Doklady 768\u2013871 (1961)"},{"issue":"1","key":"16_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01370691","volume":"31","author":"G Marongiu","year":"1991","unstructured":"Marongiu, G., Tulipani, S.: Quantifier elimination for infinite terms. Arch. Math. Log. 31(1), 1\u201317 (1991)","journal-title":"Arch. Math. Log."},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Proceedings of CAV, pp. 123\u2013136 (2006)","DOI":"10.1007\/11817963_14"},{"key":"16_CR16","unstructured":"Meister, M., Fr\u00fchwirth, T.: Complexity of the CHR rational tree equation solver. In: Proceedings of the Third Workshop on Constraint Handling Rules (2006)"},{"issue":"2","key":"16_CR17","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"issue":"4","key":"16_CR18","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1016\/j.ic.2006.08.009","volume":"205","author":"R Nieuwenhuis","year":"2007","unstructured":"Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Inf. Comput. 205(4), 557\u2013580 (2007)","journal-title":"Inf. Comput."},{"key":"16_CR19","unstructured":"Podelski, A., Roy, P.V.: The beauty and the beast algorithm: Quasi-linear incremental tests of entailment and disentailment over trees. In: International Logic Programming Symposium (ILPS), pp. 359\u2013374. MIT Press (1994)"},{"key":"16_CR20","unstructured":"Reynolds, A., Blanchette, J.C.: A decision procedure for (co)datatypes in SMT solvers. In: Kambhampati, S. (ed.) Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9\u201315 July 2016, pp. 4205\u20134209. IJCAI\/AAAI Press (2016)"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/3-540-61511-3_91","volume-title":"Automated Deduction \u2014 Cade-13","author":"S Vorobyov","year":"1996","unstructured":"Vorobyov, S.: An improved lower bound for the elementary theories of trees. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 275\u2013287. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61511-3_91"},{"key":"16_CR22","unstructured":"Zaiser, F., Ong, L.: Abstract: the extended theory of trees and algebraic (co)datatypes. In: Nadel, A., Niemetz, A. (eds.) Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification (CAV 2021), Online (initially located in Los Angeles, USA), 18\u201319 July 2021. CEUR Workshop Proceedings, vol. 2908, p.\u00a065. CEUR-WS.org (2021)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63498-7_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:36Z","timestamp":1747592256000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}