{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:45:57Z","timestamp":1762458357360},"reference-count":39,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2003,6,1]],"date-time":"2003-06-01T00:00:00Z","timestamp":1054425600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3735,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information and Computation"],"published-print":{"date-parts":[[2003,6]]},"DOI":"10.1016\/s0890-5401(03)00020-8","type":"journal-article","created":{"date-parts":[[2003,5,19]],"date-time":"2003-05-19T17:32:55Z","timestamp":1053365575000},"page":"140-164","source":"Crossref","is-referenced-by-count":85,"title":["A rewriting approach to satisfiability procedures"],"prefix":"10.1016","volume":"183","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Micha\u00ebl","family":"Rusinowitch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"2","key":"10.1016\/S0890-5401(03)00020-8_BIB1","first-page":"124","article-title":"A practical extension mechanism for decision procedures: the case study of universal presburger arithmetic","volume":"7","author":"Armando","year":"2001","journal-title":"J. Univ. Comput. Sci."},{"key":"10.1016\/S0890-5401(03)00020-8_BIB2","doi-asserted-by":"crossref","unstructured":"A. Armando, S. Ranise, M. Rusinowitch, Uniform derivation of decision procedures by superposition, in: Computer Science Logic (CSL01), Paris, France, 10\u201313 September, 2001","DOI":"10.1007\/3-540-44802-0_36"},{"issue":"3","key":"10.1016\/S0890-5401(03)00020-8_BIB3","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","article-title":"Rewrite-based equational theorem proving with selection and simplification","volume":"4","author":"Bachmair","year":"1994","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0890-5401(03)00020-8_BIB4","doi-asserted-by":"crossref","unstructured":"L. Bachmair, I.V. Ramakrishnan, A. Tiwari, L. Vigneron, Congruence closure modulo associativity and commutativity, in: Frontiers of Comb. Sys.\u2019s (FroCos\u20192000), LNCS, vol. 1794, 2000, pp. 245\u2013259","DOI":"10.1007\/10720084_16"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB5","doi-asserted-by":"crossref","unstructured":"L. Bachmair, A. Tiwari, Abstract congruence closure and specializations, in: D.A. McAllester (Ed.), 17th CADE, LNAI, vol. 1831, 2000, pp. 64\u201378","DOI":"10.1007\/10721959_5"},{"issue":"1","key":"10.1016\/S0890-5401(03)00020-8_BIB6","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1145\/363647.363681","article-title":"Automated complexity analysis based on ordered resolution","volume":"48","author":"Basin","year":"2001","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/S0890-5401(03)00020-8_BIB7","unstructured":"N. Bj\u00f8rner, Integrating decision procedures for temporal verification, Ph.D. thesis, Stanford University, 1999"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB8","unstructured":"M.P. Bonacina, On Completion Theorem Proving, January 1991, Thesis of Dottorato di Ricerca, Dipartimento di Scienze dell\u2019Informazione, Universit\u00e0 di Milano, Italy"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB9","series-title":"Proc. of the Second International Workshop on Conditional and Typed Term Rewriting Systems (CTRS-90)","first-page":"206","article-title":"Completion procedures as semidecision procedures","volume":"vol. 516","author":"Bonacina","year":"1991"},{"issue":"July","key":"10.1016\/S0890-5401(03)00020-8_BIB10","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/0304-3975(94)00187-N","article-title":"Towards a foundation of completion procedures as semidecision procedures","volume":"146","author":"Bonacina","year":"1995","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/S0890-5401(03)00020-8_BIB11","series-title":"A Computational Logic","author":"Boyer","year":"1979"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB12","first-page":"68","article-title":"Automatic verification of pipelined microprocessors control","volume":"vol. 818","author":"Burch","year":"1994"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB13","doi-asserted-by":"crossref","unstructured":"R. Caferra, N. Peltier, Decision procedures using model building techniques, in: CSL: 9th Workshop on Computer Science Logic, LNCS, vol. 1092, 1995","DOI":"10.1007\/3-540-61377-3_35"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB14","doi-asserted-by":"crossref","unstructured":"N. Dershowitz, J.-P. Jouannaud, Rewrite systems, in: J. van Leeuwen (Ed.), Hand. of Theoretical Comp. Science, 1990, pp. 243\u2013320","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"issue":"4","key":"10.1016\/S0890-5401(03)00020-8_BIB15","doi-asserted-by":"crossref","first-page":"758","DOI":"10.1145\/322217.322228","article-title":"Variations on the common subexpression problem","volume":"27","author":"Downey","year":"1980","journal-title":"J. ACM"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB16","series-title":"A Mathematical Introduction to Logic","author":"Enderton","year":"1972"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB17","series-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"Gordon","year":"1993"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB18","doi-asserted-by":"crossref","unstructured":"J. Goubault, J. Posegga, Bdds and automated deduction, 1994","DOI":"10.1007\/3-540-58495-1_54"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB19","first-page":"54","article-title":"On word problems in equational theories","volume":"vol. 267","author":"Hsiang","year":"1987"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB20","unstructured":"G. Huet, G. Kahn, C. Paulin-Mohring, The Coq Proof Assistant: a tutorial, Technical Report 204, INRIA-Rocquencourt, 1997"},{"issue":"1","key":"10.1016\/S0890-5401(03)00020-8_BIB21","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","article-title":"A complete proof of correctness of the Knuth\u2013Bendix completion algorithm","volume":"23","author":"Huet","year":"1981","journal-title":"J. Comput. Syst. Sci."},{"key":"10.1016\/S0890-5401(03)00020-8_BIB22","series-title":"Proceedings of the 8th International Conference on Rewriting Techniques and Applications","article-title":"Shostak\u2019s congruence closure as completion","volume":"vol. 1232","author":"Kapur","year":"1997"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB23","series-title":"Computational Problems in Abstract Algebra","first-page":"263","article-title":"Simple word problems in universal algebra","author":"Knuth","year":"1970"},{"issue":"1&2","key":"10.1016\/S0890-5401(03)00020-8_BIB24","first-page":"113","article-title":"On word problems in horn theories","volume":"11","author":"Kounalis","year":"1991","journal-title":"JSC"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB25","doi-asserted-by":"crossref","unstructured":"A. Leitsch, Deciding horn classes by hyperresolution, in: CSL: 3rd Workshop on Computer Science Logic, LNCS, 1990","DOI":"10.1007\/3-540-52753-2_42"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB26","doi-asserted-by":"crossref","unstructured":"C. Lynch, B. Morawska, Automatic decidability, in: Logic in Computer Science (LICS\u201902) 26 (2002) 7\u201318","DOI":"10.1109\/LICS.2002.1029813"},{"issue":"1","key":"10.1016\/S0890-5401(03)00020-8_BIB27","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1142\/S0129054192000085","article-title":"The word problem of ACD-ground theories is undecidable","volume":"3","author":"March\u00e9","year":"1992","journal-title":"Int. J. Foundations Comput. Sci."},{"key":"10.1016\/S0890-5401(03)00020-8_BIB28","doi-asserted-by":"crossref","unstructured":"P. Narendran, M. Rusinowitch, Any ground associative-commutative theory has a finite canonical system, in: 4th RTA Conf., Como, Italy, 1991","DOI":"10.1007\/3-540-53904-2_115"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB29","unstructured":"G. Nelson, Techniques for Program Verification, Technical Report CSL-81-10, Xerox Palo Alto Research Center, June 1981"},{"issue":"2","key":"10.1016\/S0890-5401(03)00020-8_BIB30","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","article-title":"Fast decision procedures based on congruence closure","volume":"27","author":"Nelson","year":"1980","journal-title":"J. ACM"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB31","unstructured":"G. Nelson, D.C. Oppen, Simplification by Cooperating Decision Procedures, Technical Report STAN-CS-78-652, Stanford CS Department, April 1978"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB32","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis, A. Rubio, Paramodulation-based theorem proving, in: A. Robinson, A. Voronkov (Eds.), Hand. of Automated Reasoning, 2001","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB33","series-title":"11th International Conference on Automated Deduction (CADE), Saratoga, NY","first-page":"748","article-title":"PVS: a prototype verification system","volume":"vol. 607","author":"Owre","year":"1992"},{"issue":"2","key":"10.1016\/S0890-5401(03)00020-8_BIB34","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1006\/inco.1996.0028","article-title":"Proof lengths for equational completion","volume":"125","author":"Plaisted","year":"1996","journal-title":"Inform. Comput."},{"issue":"1&2","key":"10.1016\/S0890-5401(03)00020-8_BIB35","first-page":"21","article-title":"Theorem-proving with resolution and superposition","volume":"11","author":"Rusinowitch","year":"1991","journal-title":"JSC"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB36","series-title":"Proc. of the 1st IJCAR, Siena","first-page":"370","article-title":"System abstract: E 0.61","volume":"vol. 2083","author":"Schulz","year":"2001"},{"issue":"1","key":"10.1016\/S0890-5401(03)00020-8_BIB37","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","article-title":"Deciding combination of theories","volume":"31","author":"Shostak","year":"1984","journal-title":"J. ACM"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB38","doi-asserted-by":"crossref","unstructured":"A. Stump, D.L. Dill, C.W. Barrett, J. Levitt, A decision procedure for an extensional theory of arrays, in: LICS\u201901, 2001","DOI":"10.1109\/LICS.2001.932480"},{"key":"10.1016\/S0890-5401(03)00020-8_BIB39","series-title":"The Design and Analysis of Computer Algorithms","author":"Ullman","year":"1974"}],"container-title":["Information and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540103000208?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540103000208?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,18]],"date-time":"2020-03-18T10:02:34Z","timestamp":1584525754000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0890540103000208"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,6]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,6]]}},"alternative-id":["S0890540103000208"],"URL":"https:\/\/doi.org\/10.1016\/s0890-5401(03)00020-8","relation":{},"ISSN":["0890-5401"],"issn-type":[{"value":"0890-5401","type":"print"}],"subject":[],"published":{"date-parts":[[2003,6]]}}}