{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:19:51Z","timestamp":1725664791865},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614647"},{"type":"electronic","value":"9783540685968"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61464-8_40","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:40:27Z","timestamp":1330292427000},"page":"18-32","source":"Crossref","is-referenced-by-count":2,"title":["AC-complete unification and its application to theorem proving"],"prefix":"10.1007","author":[{"given":"Alexandre","family":"Boudet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Evelyne","family":"Contejean","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claude","family":"March\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"3_CR1","volume-title":"LNAI 607","author":"F. Baader","year":"1992","unstructured":"F. Baader and K. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In D. Kapur, editor, Proc. 11th Int. Conf. on Automated Deduction, Saratoga Springs, NY, LNAI 607, 1992."},{"issue":"1","key":"3_CR2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0747-7171(88)80018-X","volume":"6","author":"L. Bachmair","year":"1988","unstructured":"L. Bachmair and N. Dershowitz. Critical pair criteria for completion. Journal of Symbolic Computation, 6(1):1\u201318, 1988.","journal-title":"Journal of Symbolic Computation"},{"issue":"2&3","key":"3_CR3","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0304-3975(89)90003-0","volume":"67","author":"L. Bachmair","year":"1989","unstructured":"L. Bachmair and N. Dershowitz. Completion for rewriting modulo a congruence. Theoretical Comput. Sci., 67(2&3):173\u2013201, Oct. 1989.","journal-title":"Theoretical Comput. Sci."},{"key":"3_CR4","volume-title":"LNAI 607","author":"L. Bachmair","year":"1992","unstructured":"L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation and superposition. In D. Kapur, editor, Proc. 11th Int. Conf. on Automated Deduction, Saratoga Springs, NY, LNAI 607. Springer-Verlag, June 1992."},{"key":"3_CR5","series-title":"LNCS 355","first-page":"29","volume-title":"Complete sets of reductions modulo Associativity, Commutativity and Identity","year":"1989","unstructured":"T. Baird, G. Peterson, and R. Wilkerson. Complete sets of reductions modulo Associativity, Commutativity and Identity. In Proc. 3rd Rewriting Techniques and Applications, Chapel Hill, LNCS 355, pages 29\u201344. Springer-Verlag, Apr. 1989."},{"key":"3_CR6","volume-title":"Th\u00e8se de doctorat","author":"A. Boudet","year":"1990","unstructured":"A. Boudet. Unification dans les M\u00e9langes de Th\u00e9ories \u00e9quationnelles. Th\u00e8se de doctorat, Universit\u00e9 Paris-Sud, Orsay, France, Feb. 1990."},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1006\/jsco.1993.1066","volume":"16","author":"A. Boudet","year":"1993","unstructured":"A. Boudet. Combining unification algorithms. Journal of Symbolic Computation, 16:597\u2013626, 1993.","journal-title":"Journal of Symbolic Computation"},{"key":"3_CR8","first-page":"289","volume-title":"A new AC-unification algorithm with a new algorithm for solving diophantine equations","author":"A. Boudet","year":"1990","unstructured":"A. Boudet, E. Contejean, and H. Devie. A new AC-unification algorithm with a new algorithm for solving diophantine equations. In Proc. 5th IEEE Symp. Logic in Computer Science, Philadelphia, pages 289\u2013299. IEEE Computer Society Press, June 1990."},{"key":"3_CR9","volume-title":"PhD thesis","author":"B. Buchberger","year":"1965","unstructured":"B. Buchberger. An Algorithm for Finding a Basis for the Residue Class Ring of a Zero-Dimensional Ideal. PhD thesis, University of Innsbruck, Austria, 1965. (in German)."},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"B. Buchberger and R. Loos. Algebraic simplification. In Computer Algebra, Symbolic and Algebraic Computation. Computing Supplementum 4. Springer-Verlag, 1982.","DOI":"10.1007\/978-3-7091-3406-1_2"},{"key":"3_CR11","volume-title":"LNCS 310","author":"H. J. B\u00fcrckert","year":"1988","unstructured":"H. J. B\u00fcrckert. Solving disequations in equational theories. In Proc. 9th Int. Conf. on Automated Deduction, Argonne, IL, LNCS 310. Springer-Verlag, May 1988."},{"issue":"6","key":"3_CR12","doi-asserted-by":"crossref","first-page":"537","DOI":"10.1016\/S0747-7171(19)80001-9","volume":"14","author":"E. Domenjoud","year":"1992","unstructured":"E. Domenjoud. AC unification through order-sorted AC1 unification. Journal of Symbolic Computation, 14(6):537\u2013556, Dec. 1992.","journal-title":"Journal of Symbolic Computation"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"F. Fages. Associative-commutative unification. Journal of Symbolic Computation, 3(3), June 1987.","DOI":"10.1016\/S0747-7171(87)80004-4"},{"issue":"3","key":"3_CR14","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/BF00243791","volume":"3","author":"A. Herold","year":"1987","unstructured":"A. Herold and J. H. Siekmann. Unification in abelian semi-groups. Journal of Automated Reasoning, 3(3):247\u2013283, 1987.","journal-title":"Journal of Automated Reasoning"},{"key":"3_CR15","unstructured":"J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT-Press, 1991."},{"issue":"4","key":"3_CR16","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM J. Comput., 15(4):1155\u20131194, 1986.","journal-title":"SIAM J. Comput."},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/0304-3975(92)90165-C","volume":"104","author":"J.-P. Jouannaud","year":"1992","unstructured":"J.-P. Jouannaud and C. March\u00e9. Termination and completion modulo associativity, commutativity and identity. Theoretical Comput. Sci., 104:29\u201351, 1992.","journal-title":"Theoretical Comput. Sci."},{"key":"3_CR18","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/S0747-7171(88)80019-1","volume":"4","author":"D. Kapur","year":"1988","unstructured":"D. Kapur, D. Musser, and P. Narendran. Only prime superpositions need be considered for the Knuth-Bendix procedure. Journal of Symbolic Computation, 4:19\u201336, 1988.","journal-title":"Journal of Symbolic Computation"},{"key":"3_CR19","volume-title":"Th\u00e8se d'Etat","author":"C. Kirchner","year":"1985","unstructured":"C. Kirchner. M\u00e9thodes et outils de conception syst\u00e9matique d'algorithmes d'unification dans les th\u00e9ories equationnelles. Th\u00e8se d'Etat, Univ. Nancy, France, 1985."},{"key":"3_CR20","unstructured":"C. Kirchner, editor. Unification. Academic Press, 1990."},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"D. E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"3_CR22","volume-title":"Research Report Memo ATP-37","author":"D. S. Lankford","year":"1977","unstructured":"D. S. Lankford and A. M. Ballantyne. Decision procedures for simple equational theories with permutative axioms: Complete sets of permutative reductions. Research Report Memo ATP-37, Department of Mathematics and Computer Science, University of Texas, Austin, Texas, USA, Aug. 1977."},{"key":"3_CR23","first-page":"214","volume-title":"Informatik Fachberichte, Vol. 47","author":"R. Loos","year":"1981","unstructured":"R. Loos. Term reduction systems and algebraic algorithms. In Proceedings of the Fifth GI Workshop on Artificial Intelligence, pages 214\u2013234, Bad Honnef, West Germany, 1981. Available as Informatik Fachberichte, Vol. 47."},{"key":"3_CR24","first-page":"394","volume-title":"Normalised rewriting and normalised completion","author":"C. March\u00e9","year":"1994","unstructured":"C. March\u00e9. Normalised rewriting and normalised completion. In Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science, pages 394\u2013403, Paris, France, July 1994. IEEE Comp. Soc. Press."},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"C. March\u00e9. Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation, 1996. to appear.","DOI":"10.1006\/jsco.1996.0011"},{"key":"3_CR26","first-page":"371","volume-title":"LNCS 582","author":"R. Nieuwenhuis","year":"1992","unstructured":"R. Nieuwenhuis and A. Rubio. Basic superposition is complete. In B. Krieg-Bruckner, editor, Proc. European Symp. on Programming, LNCS 582, pages 371\u2013389, Rennes, 1992. Springer-Verlag."},{"key":"3_CR27","volume-title":"AC-superposition with constraints: no AC unifier needed","author":"R. Nieuwenhuis","year":"1994","unstructured":"R. Nieuwenhuis and A. Rubio. AC-superposition with constraints: no AC unifier needed. In Proc. 12th Int. Conf. on Automated Deduction, LNAI, Nancy, June 1994. Springer-Verlag."},{"issue":"2","key":"3_CR28","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. E. Peterson","year":"1981","unstructured":"G. E. Peterson and M. E. Stickel. Complete sets of reductions for some equational theories. J. ACM, 28(2):233\u2013264, Apr. 1981.","journal-title":"J. ACM"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"M. Schmidt-Schau\u00df. Unification in a combination of arbitrary disjoint equational theories. Journal of Symbolic Computation, 1990. Special issue on Unification.","DOI":"10.1016\/S0747-7171(89)80022-7"},{"issue":"3","key":"3_CR30","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"M. Stickel","year":"1981","unstructured":"M. Stickel. A unification algorithm for associative-commutative functions. J. ACM, 28(3):423\u2013434, 1981.","journal-title":"J. ACM"},{"key":"3_CR31","volume-title":"Associative commutative deduction with constraints","author":"L. Vigneron","year":"1994","unstructured":"L. Vigneron. Associative commutative deduction with constraints. In Proc. 12th Int. Conf. on Automated Deduction, LNAI, Nancy, June 1994. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61464-8_40.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T10:35:59Z","timestamp":1640946959000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61464-8_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614647","9783540685968"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-61464-8_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}