{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,10]],"date-time":"2025-12-10T08:59:42Z","timestamp":1765357182381},"reference-count":13,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,8,12]],"date-time":"2022-08-12T00:00:00Z","timestamp":1660262400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,8,12]],"date-time":"2022-08-12T00:00:00Z","timestamp":1660262400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,11]]},"DOI":"10.1007\/s10817-022-09635-1","type":"journal-article","created":{"date-parts":[[2022,8,12]],"date-time":"2022-08-12T18:03:00Z","timestamp":1660327380000},"page":"845-860","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Faster Linear Unification Algorithm"],"prefix":"10.1007","volume":"66","author":[{"given":"Dennis","family":"de Champeaux","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,12]]},"reference":[{"key":"9635_CR1","volume-title":"Handbook Of Automated Reasoning","author":"F Baader","year":"2001","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) Handbook Of Automated Reasoning. Elsevier, Amsterdam (2001)"},{"issue":"1","key":"9635_CR2","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0022-0000(86)90003-6","volume":"32","author":"D de Champeaux","year":"1986","unstructured":"de Champeaux, D.: About the Paterson\u2013Wegman linear unification algorithm. J. Comput. Syst. Sci. 32(1), 79\u201390 (1986). https:\/\/doi.org\/10.1016\/0022-0000(86)90003-6","journal-title":"J. Comput. Syst. Sci."},{"key":"9635_CR3","unstructured":"Jacobson, E.: Unification and anti-unification. Technical Report (1991). http:\/\/erikjacobsen.com\/pdf\/unification.pdf"},{"key":"9635_CR4","unstructured":"https:\/\/github.com\/ddccc\/Unification. Accessed 24 July 2022"},{"key":"9635_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04617-9_55","volume-title":"KI 2009: Advances in Artificial Intelligence","author":"K Hoder","year":"2009","unstructured":"Hoder, K., Voronkov, A.: Comparing unification algorithms in first-order theorem proving. In: Mertsching, B., Hund, M., Aziz, Z. (eds.) KI 2009: Advances in Artificial Intelligence. Lecture Notes in Computer Science, vol. 5803. Springer, Berlin (2009). https:\/\/doi.org\/10.1007\/978-3-642-04617-9_55"},{"issue":"4","key":"9635_CR6","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1145\/321906.321919","volume":"22","author":"R Kowalski","year":"1975","unstructured":"Kowalski, R.: A proof procedure using connection graphs. J. Assoc. Comput. Mach. 22(4), 572\u2013659 (1975). https:\/\/doi.org\/10.1145\/321906.321919","journal-title":"J. Assoc. Comput. Mach."},{"key":"9635_CR7","unstructured":"Martelli, A., Montanari, U.: Unification in linear time and space: a structured presentation. Internal Report B76-16. Ist. di Elaborazione delle Informazione, Consiglio Nazionale delle Ricerche, Pisa, Italy (1976)"},{"issue":"2","key":"9635_CR8","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A Martelli","year":"1982","unstructured":"Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. Program. Lang. Syst. 4(2), 258\u2013282 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9635_CR9","unstructured":"Motroi, V., Ciobaco, S.: A Typo in the Paterson\u2013Wegman\u2013de Champeaux algorithm. Arxiv Preprint (2020). https:\/\/arxiv.org\/abs\/2007.00304"},{"issue":"2","key":"9635_CR10","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"MS Paterson","year":"1978","unstructured":"Paterson, M.S., Wegman, M.N.: Linear unification. J. Comput. Syst. Sci. 16(2), 158\u2013167 (1978). https:\/\/doi.org\/10.1016\/0022-0000(78)90043-0","journal-title":"J. Comput. Syst. Sci."},{"key":"9635_CR11","unstructured":"https:\/\/en.wikipedia.org\/wiki\/Planning_Domain_Definition_Language. Accessed 24 July 2022"},{"issue":"1","key":"9635_CR12","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. Assoc. Comput. Mach. 12(1), 23\u201341 (1965)","journal-title":"J. Assoc. Comput. Mach."},{"key":"9635_CR13","unstructured":"https:\/\/en.wikipedia.org\/wiki\/Disjoint-set_data_structure. Accessed 24 July 2022"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09635-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09635-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09635-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,5]],"date-time":"2022-11-05T11:20:08Z","timestamp":1667647208000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09635-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,12]]},"references-count":13,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,11]]}},"alternative-id":["9635"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09635-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,12]]},"assertion":[{"value":"5 November 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 June 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 August 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"There are no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}