{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:17:19Z","timestamp":1725484639601},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425540"},{"type":"electronic","value":"9783540448020"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44802-0_36","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T00:15:38Z","timestamp":1180656938000},"page":"513-527","source":"Crossref","is-referenced-by-count":20,"title":["Uniform Derivation of Decision Procedures by Superposition"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[]},{"given":"Micha\u00ebl","family":"Rusinowitch","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,30]]},"reference":[{"issue":"2","key":"36_CR1","first-page":"124","volume":"7","author":"A. Armando","year":"2001","unstructured":"A. Armando and S. Ranise. A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic. J. of Universal Computer Science, 7(2):124\u2013140, February 2001.","journal-title":"J. of Universal Computer Science"},{"issue":"3","key":"36_CR2","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. J. of Logic and Comp., 4(3):217\u2013247, 1994.","journal-title":"J. of Logic and Comp."},{"key":"36_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/10720084_16","volume-title":"Frontiers of Comb. Sys.\u2019s (FroCos\u20192000)","author":"L. Bachmair","year":"2000","unstructured":"L. Bachmair, I. V. Ramakrishnan, A. Tiwari, and L. Vigneron. Congruence closure modulo associativity and commutativity. In Frontiers of Comb. Sys.\u2019s (FroCos\u20192000), LNCS 1794, pages 245\u2013259, 2000."},{"key":"36_CR4","doi-asserted-by":"crossref","unstructured":"L. Bachmair and A. Tiwari. Abstract congruence closure and specializations. In D. A. McAllester, editor, 17th CADE, LNAI 1831, pages 64\u201378, 2000.","DOI":"10.1007\/10721959_5"},{"key":"36_CR5","series-title":"Lect Notes Comput Sci","volume-title":"CSL: 9th Workshop on Computer Science Logic","author":"R. Caferra","year":"1995","unstructured":"R. Caferra and Peltier. Decision procedures using model building techniques. In CSL: 9th Workshop on Computer Science Logic. LNCS 1092, 1995."},{"key":"36_CR6","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Hand. of Theoretical Comp. Science, pages 243\u2013320. 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"36_CR7","unstructured":"H. B. Enderton. A Mathematical Introduction to Logic. Academic Pr., 1972."},{"key":"36_CR8","doi-asserted-by":"crossref","unstructured":"D. E. Knuth and P. E. Bendix. Simple word problems in universal algebra. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297, Oxford, 1970. Pergamon Press.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"36_CR9","doi-asserted-by":"crossref","unstructured":"E. Kounalis and M. Rusinowitch. On Word Problems in Horn Theories. JSC, 11(1&2):113\u2013128, January\/February 1991.","DOI":"10.1016\/S0747-7171(08)80134-4"},{"key":"36_CR10","series-title":"Lect Notes Comput Sci","volume-title":"CSL: 3rd Workshop on Computer Science Logic","author":"A. Leitsch","year":"1990","unstructured":"A. Leitsch. Deciding horn classes by hyperresolution. In CSL: 3rd Workshop on Computer Science Logic. LNCS, 1990."},{"issue":"1","key":"36_CR11","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1142\/S0129054192000085","volume":"3","author":"C. March\u00e9","year":"1992","unstructured":"C. March\u00e9. The word problem of ACD-ground theories is undecidable. International Journal of Foundations of Computer Science, 3(1):81\u201392, 1992.","journal-title":"International Journal of Foundations of Computer Science"},{"key":"36_CR12","unstructured":"G. Nelson. Techniques for Program Verification. Technical Report CSL-81-10, Xerox Palo Alto Research Center, June 1981."},{"key":"36_CR13","unstructured":"G. Nelson and D.C. Oppen. Simplification by Cooperating Decision Procedures. Technical Report STAN-CS-78-652, Stanford CS Dept., April 1978."},{"issue":"2","key":"36_CR14","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Greg Nelson and Derek C. Oppen. Fast decision procedures based on congruence closure. Journal of the ACM, 27(2):356\u2013364, 1980.","journal-title":"Journal of the ACM"},{"key":"36_CR15","doi-asserted-by":"crossref","unstructured":"P. Narendran and 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":"36_CR16","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and A. Rubio. Paramodulation-based theorem proving. In A. Robinson and A. Voronkov, editors, Hand. of Automated Reasoning. 2001.","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"issue":"1&2","key":"36_CR17","first-page":"21","volume":"11","author":"M. Rusinowitch","year":"1991","unstructured":"M. Rusinowitch. Theorem-proving with Resolution and Superposition. JSC, 11(1&2):21\u201350, January\/February 1991.","journal-title":"JSC"},{"key":"36_CR18","doi-asserted-by":"crossref","unstructured":"A. Stump, D. L. Dill, C. W. Barrett, and J. Levitt. A Decision Procedure for an Extensional Theory of Arrays. In LICS\u201901, 2001. To appear.","DOI":"10.1109\/LICS.2001.932480"},{"key":"36_CR19","volume-title":"The Design and Analysis of Computer Algorithms","author":"J. D. Ullman","year":"1974","unstructured":"J. D. Ullman, A. V. Aho, and J. E. Hopcroft. The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, 1974."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44802-0_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:21:11Z","timestamp":1556450471000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44802-0_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425540","9783540448020"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-44802-0_36","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}