{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:21:17Z","timestamp":1750306877180,"version":"3.41.0"},"reference-count":0,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[1987,5,1]],"date-time":"1987-05-01T00:00:00Z","timestamp":546825600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSAM Bull."],"published-print":{"date-parts":[[1987,5]]},"abstract":"<jats:p>The unification problem for terms containing associative and commutative functions is of great importance in theorem provers based on the rewriting approach and resolution methods. The complexity of checking whether two such terms are unifiable was known to be NP-hard. It is proved that the problem is NP-complete by describing a nondeterministic polynomial time algorithm for it. It is also shown that if in addition, an associative-commutative function is assumed to be idempotent and\/or have an identity, the problem still remains NP-complete.<\/jats:p>","DOI":"10.1145\/24554.1095562","type":"journal-article","created":{"date-parts":[[2007,1,17]],"date-time":"2007-01-17T18:32:02Z","timestamp":1169058722000},"page":"25-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Abstracts of Technical Reports Computer Science Branch, Corporate Research and Development, General Electric Company, Schenectady, NY 12345 (GE)"],"prefix":"10.1145","volume":"21","member":"320","published-online":{"date-parts":[[1987,5]]},"container-title":["ACM SIGSAM Bulletin"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/24554.1095562","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/24554.1095562","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:18:26Z","timestamp":1750234706000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/24554.1095562"}},"subtitle":[],"editor":[{"given":"Franz","family":"Winkler","sequence":"first","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]}],"short-title":[],"issued":{"date-parts":[[1987,5]]},"references-count":0,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1987,5]]}},"alternative-id":["10.1145\/24554.1095562"],"URL":"https:\/\/doi.org\/10.1145\/24554.1095562","relation":{},"ISSN":["0163-5824"],"issn-type":[{"type":"print","value":"0163-5824"}],"subject":[],"published":{"date-parts":[[1987,5]]},"assertion":[{"value":"1987-05-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}