{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:24Z","timestamp":1760202624241,"version":"3.41.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T00:00:00Z","timestamp":1309478400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"LOGICTOOLS-2","award":["TIN2007-68093-C02-01"],"award-info":[{"award-number":["TIN2007-68093-C02-01"]}]},{"DOI":"10.13039\/501100003176","name":"Ministerio de Educaci\u00f3n, Cultura y Deporte","doi-asserted-by":"publisher","award":["TIN2007-66523"],"award-info":[{"award-number":["TIN2007-66523"]}],"id":[{"id":"10.13039\/501100003176","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2011,7]]},"abstract":"<jats:p>Term unification plays an important role in many areas of computer science, especially in those related to logic. The universal mechanism of grammar-based compression for terms, in particular the so-called<jats:italic>singleton tree grammars (STGAs)<\/jats:italic>, have recently drawn considerable attention. Using STGs, terms of exponential size and height can be represented in linear space. Furthermore, the term representation by directed acyclic graphs (dags) can be efficiently simulated. The present article is the result of an investigation on term unification and matching when the terms given as input are represented using different compression mechanisms for terms such as dags and singleton tree grammars. We describe a polynomial time algorithm for context matching with dags, when the number of different context variables is fixed for the problem. For the same problem, NP-completeness is obtained when the terms are represented using the more general formalism of singleton tree grammars. For first-order unification and matching polynomial time algorithms are presented, each of them improving previous results for those problems.<\/jats:p>","DOI":"10.1145\/1970398.1970402","type":"journal-article","created":{"date-parts":[[2011,7,21]],"date-time":"2011-07-21T13:27:09Z","timestamp":1311254829000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Unification and matching on compressed terms"],"prefix":"10.1145","volume":"12","author":[{"given":"Adri\u00e0","family":"Gasc\u00f3n","sequence":"first","affiliation":[{"name":"Universitat Polit\u00e8cnica de Catalunya, Barcelona, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillem","family":"Godoy","sequence":"additional","affiliation":[{"name":"Universitat Polit\u00e8cnica de Catalunya, Barcelona, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manfred","family":"Schmidt-Schauss","sequence":"additional","affiliation":[{"name":"Goethe-Universit\u00e4t, Frankfurt, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,7,22]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Baader F. and Siekmann J. 1994. Unification theory. In Handbook of Logic in Artificial Intelligence and Logic Programming D. Gabbay C. Hogger and J. Robinson Eds. Oxford University Press Oxford U.K. 41--125. Baader F. and Siekmann J. 1994. Unification theory. In Handbook of Logic in Artificial Intelligence and Logic Programming D. Gabbay C. Hogger and J. Robinson Eds. Oxford University Press Oxford U.K. 41--125.","DOI":"10.1093\/oso\/9780198537465.003.0002"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Baader F. and Snyder W. 2001. Unification theory. In Handbook of Automated Reasoning J. A. Robinson and A.Voronkov Eds. Elsevier and MIT Press Amsterdam The Netherlands and Cambridge MA 445--532. Baader F. and Snyder W. 2001. Unification theory. In Handbook of Automated Reasoning J. A. Robinson and A.Voronkov Eds. Elsevier and MIT Press Amsterdam The Netherlands and Cambridge MA 445--532.","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"volume":"202","volume-title":"Proceedings of the International Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science","author":"Benanav D.","key":"e_1_2_1_3_1"},{"volume-title":"Eds","year":"2007","author":"Berglund A.","key":"e_1_2_1_4_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2002.1852"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11601524_13"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2008.01.004"},{"key":"e_1_2_1_9_1","unstructured":"Comon H. Dauchet M. Gilleron R. Jacquemard F. Lugiez D. Tison S. and Tommasi M. 1997. Tree automata techniques and applications. http:\/\/www.grappa.univ-lille3.fr\/tata. Comon H. Dauchet M. Gilleron R. Jacquemard F. Lugiez D. Tison S. and Tommasi M. 1997. Tree automata techniques and applications. http:\/\/www.grappa.univ-lille3.fr\/tata."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322228"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.17"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_26"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2008.10.005"},{"volume":"1075","volume-title":"Proceedings of the 7th Annual Symposium on Combinational Pattern Matching. Lecture Notes in Computer Science","author":"Gasieniec L.","key":"e_1_2_1_14_1"},{"volume-title":"Proceedings of the Latin American Symposium on Theoretical Informatics. Springer-Verlag","author":"Genest B.","key":"e_1_2_1_15_1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1131342.1131345"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/647194.720822"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/647194.720822"},{"volume":"4421","volume-title":"Proceedings of the European Symposium on Programming (ESOP). Lecture Notes in Computer Science","author":"Gulwani S.","key":"e_1_2_1_19_1"},{"volume-title":"Proceedings of the International Symposium on String Processing and Informational Retrieval '00","author":"Hirao M.","key":"e_1_2_1_20_1"},{"volume-title":"Proceedings of the 4th Scandinavian Workshop on Algorithm Theory. Springer-Verlag","author":"Karpinski M.","key":"e_1_2_1_21_1"},{"volume-title":"Proceedings of the Annual Symposium on Combinational Pattern Matching. Springer-Verlag","author":"Karpinski M.","key":"e_1_2_1_22_1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11821069_56"},{"volume":"3091","volume-title":"Proceedings of the 15th International Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science","author":"Levy J.","key":"e_1_2_1_24_1"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_30"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_8"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1137\/050645403"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Levy J. Schmidt-Schauss M. and Villaret M. 2010. On the complexity of bounded second-order unification and stratified context unification. J. Alg. Cogn. Inform. Logic. To appear. Levy J. Schmidt-Schauss M. and Villaret M. 2010. On the complexity of bounded second-order unification and stratified context unification. J. Alg. Cogn. Inform. Logic. To appear.","DOI":"10.1093\/jigpal\/jzq010"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/2394373.2394405"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539704445950"},{"volume-title":"Proceedings of the 10th International Conference on Implemantation and Application of Automate.","author":"Lohrey M.","key":"e_1_2_1_31_1"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/3266641.3266666"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/DEXA.2008.41"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/357162.357169"},{"volume-title":"Proceedings of the 8th Annual Symposium on Combinational Pattern Matching. 1264 Lecture Notes in Computer Science. Springer-Verlag","author":"Miyazaki M.","key":"e_1_2_1_35_1"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.3115\/976909.979670"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90043-0"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/647904.739319"},{"key":"e_1_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Plandowski W. and Rytter W. 1999. Complexity of language recognition problems for compressed words. In Jewels are Forever. Springer Berlin Germany 262--272. Plandowski W. and Rytter W. 1999. Complexity of language recognition problems for compressed words. In Jewels are Forever. Springer Berlin Germany 262--272.","DOI":"10.1007\/978-3-642-60207-8_23"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"volume-title":"Polynomial equality testing for terms with shared substructures. Frank rep. 21","author":"Schmidt-Schauss M.","key":"e_1_2_1_42_1"},{"volume":"1379","volume-title":"Proceedings of the 9th International Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science","author":"Schmidt-Schauss M.","key":"e_1_2_1_43_1"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2001.0438"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-004-1151-9"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1977.1055714"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1970398.1970402","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1970398.1970402","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:52:53Z","timestamp":1750243973000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1970398.1970402"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7]]},"references-count":44,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,7]]}},"alternative-id":["10.1145\/1970398.1970402"],"URL":"https:\/\/doi.org\/10.1145\/1970398.1970402","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2011,7]]},"assertion":[{"value":"2010-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-07-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}