{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T13:13:13Z","timestamp":1791033193254,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642340048","type":"print"},{"value":"9783642340055","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34005-5_12","type":"book-chapter","created":{"date-parts":[[2012,10,3]],"date-time":"2012-10-03T02:33:39Z","timestamp":1349231619000},"page":"221-239","source":"Crossref","is-referenced-by-count":1,"title":["A Rule-Based Framework for Building Superposition-Based Decision Procedures"],"prefix":"10.1007","author":[{"given":"Elena","family":"Tushkanova","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alain","family":"Giorgetti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christophe","family":"Ringeissen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Olga","family":"Kouchnarenko","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1) (2009)","DOI":"10.1145\/1459010.1459014"},{"issue":"2","key":"12_CR2","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A. Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput.\u00a0183(2), 140\u2013164 (2003)","journal-title":"Inf. Comput."},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-642-02348-4_27","volume-title":"Rewriting Techniques and Applications","author":"M. Clavel","year":"2009","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Escobar, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Unification and Narrowing in Maude 2.4. In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 380\u2013390. Springer, Heidelberg (2009)"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science (2001)","DOI":"10.1016\/S0304-3975(01)00359-0"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Formal Models and Semantics, vol.\u00a0B, pp. 243\u2013320. MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-16310-4_6","volume-title":"Rewriting Logic and Its Applications","author":"F. Dur\u00e1n","year":"2010","unstructured":"Dur\u00e1n, F., Meseguer, J.: A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol.\u00a06381, pp. 69\u201385. Springer, Heidelberg (2010)"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-642-16310-4_7","volume-title":"Rewriting Logic and Its Applications","author":"F. Dur\u00e1n","year":"2010","unstructured":"Dur\u00e1n, F., Meseguer, J.: A Maude Coherence Checker Tool for Conditional Order-Sorted Rewrite Theories. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol.\u00a06381, pp. 86\u2013103. Springer, Heidelberg (2010)"},{"issue":"11","key":"12_CR8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2006.03.017","volume":"174","author":"S. Eker","year":"2007","unstructured":"Eker, S., Mart\u00ed-Oliet, N., Meseguer, J., Verdejo, A.: Deduction, strategies, and rewriting. Electr. Notes Theor. Comput. Sci.\u00a0174(11), 3\u201325 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"7","key":"12_CR9","doi-asserted-by":"publisher","first-page":"1026","DOI":"10.1016\/j.ic.2011.03.005","volume":"209","author":"C. Lynch","year":"2011","unstructured":"Lynch, C., Ranise, S., Ringeissen, C., Tran, D.K.: Automatic decidability and combinability. Inf. Comput.\u00a0209(7), 1026\u20131047 (2011)","journal-title":"Inf. Comput."},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Lynch, C., Morawska, B.: Automatic decidability. In: Proc. of 17th IEEE Symposium on Logic in Computer Science (LICS 2002), Copenhagen, Denmark, pp. 7\u201316. IEEE Computer Society Press (2002)","DOI":"10.1109\/LICS.2002.1029813"},{"key":"12_CR11","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1016\/j.entcs.2004.06.020","volume":"117","author":"N. Mart\u00ed-Oliet","year":"2005","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J., Verdejo, A.: Towards a strategy language for Maude. Electr. Notes Theor. Comput. Sci.\u00a0117, 417\u2013441 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"12_CR12","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-02959-2_4","volume-title":"Automated Deduction \u2013 CADE-22","author":"E. Nicolini","year":"2009","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Combinable Extensions of Abelian Groups. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol.\u00a05663, pp. 51\u201366. Springer, Heidelberg (2009)"},{"issue":"1-2","key":"12_CR13","doi-asserted-by":"crossref","first-page":"163","DOI":"10.3233\/FI-2010-362","volume":"105","author":"E. Nicolini","year":"2010","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Combining satisfiability procedures for unions of theories with a shared counting operator. Fundamenta Informaticae\u00a0105(1-2), 163\u2013187 (2010)","journal-title":"Fundamenta Informaticae"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 371\u2013443. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"issue":"2-3","key":"12_CR15","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun.\u00a015(2-3), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"12_CR16","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C. Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol.\u00a05663, pp. 140\u2013145. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34005-5_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T22:14:54Z","timestamp":1744236894000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34005-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642340048","9783642340055"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34005-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}