{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:29:15Z","timestamp":1725568155912},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_15","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T09:13:30Z","timestamp":1288084410000},"page":"182-196","source":"Crossref","is-referenced-by-count":5,"title":["Superposition Modulo a Shostak Theory"],"prefix":"10.1007","author":[{"given":"Harald","family":"Ganzinger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Hillenbrand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"15_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation\u00a04(3), 217\u2013247 (1994)","journal-title":"Journal of Logic and Computation"},{"issue":"3\/4","key":"15_CR2","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Applicable Algebra in Engineering, Communication and Computing\u00a05(3\/4), 193\u2013212 (1994)","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"15_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"15_CR4","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/3-540-52885-7_87","volume-title":"10th International Conference on Automated Deduction","author":"H.-J. B\u00fcrckert","year":"1990","unstructured":"B\u00fcrckert, H.-J.: A resolution principle for clauses with constraints. In: Stickel, M.E. (ed.) CADE 1990. LNCS (LNAI), vol.\u00a0449, pp. 178\u2013192. Springer, Heidelberg (1990)"},{"key":"15_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/3-540-45620-1_28","volume-title":"Automated Deduction - CADE-18","author":"H. Ganzinger","year":"2002","unstructured":"Ganzinger, H.: Shostak light. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 332\u2013346. Springer, Heidelberg (2002)"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hillenbrand, T., Waldmann, U.: Superposition modulo a Shostak theory. Technical report, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken (2003)","DOI":"10.1007\/978-3-540-45085-6_15"},{"key":"15_CR7","first-page":"413","volume-title":"Proceedings of the 15th IEEE Symposium on Logic in Computer Science","author":"G. Godoy","year":"2000","unstructured":"Godoy, G., Nieuwenhuis, R.: Paramodulation with built-in abelian groups. In: Proceedings of the 15th IEEE Symposium on Logic in Computer Science, pp. 413\u2013424. IEEE Computer Society Press, Los Alamitos (2000)"},{"issue":"1","key":"15_CR8","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/0304-3975(92)90165-C","volume":"104","author":"J.-P. Jouannaud","year":"1992","unstructured":"Jouannaud, J.-P., March\u00b4e, C.: Termination and completion modulo associativity, commutativity and identity. Theoretical Computer Science\u00a0104(1), 29\u201351 (1992)","journal-title":"Theoretical Computer Science"},{"key":"15_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/3-540-45988-X_8","volume-title":"Frontiers of Combining Systems","author":"D. Kapur","year":"2002","unstructured":"Kapur, D.: A rewrite rule based framework for combining decision procedures. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol.\u00a02309, pp. 87\u2013102. Springer, Heidelberg (2002)"},{"key":"15_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-540-45085-6_16","volume-title":"Automated Deduction \u2013 CADE-19","author":"S. Krsti\u0107","year":"2003","unstructured":"Krsti\u0107, S., Conchon, S.: Canonization for disjoint unions of theories. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 197\u2013211. Springer, Heidelberg (2003)"},{"key":"15_CR11","volume-title":"Canonical Forms in Finitely Presented Algebras","author":"P. Chenadec Le","year":"1986","unstructured":"Le Chenadec, P.: Canonical Forms in Finitely Presented Algebras. John Wiley & Sons, Chichester (1986)"},{"key":"15_CR12","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1109\/LICS.1994.316050","volume-title":"Proceedings of the 9th IEEE Symposium on Logic in Computer Science","author":"C. March\u00e9","year":"1994","unstructured":"March\u00e9, C.: Normalised rewriting and normalised completion. In: Proceedings of the 9th IEEE Symposium on Logic in Computer Science, pp. 394\u2013403. IEEE Computer Society Press, Los Alamitos (1994)"},{"key":"15_CR13","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/3-540-58156-1_33","volume-title":"Automated Deduction - CADE-12","author":"A. Middeldorp","year":"1994","unstructured":"Middeldorp, A., Zantema, H.: Simple termination revisited. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 451\u2013465. Springer, Heidelberg (1994)"},{"issue":"2","key":"15_CR14","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"15_CR15","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning, ch. 7","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 7, vol.\u00a0I, pp. 371\u2013443. Elsevier, Amsterdam (2001)"},{"key":"15_CR16","unstructured":"Plotkin, G.D.: Building-in equational theories. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence 7, ch. 4, pp. 73\u201390. American Elsevier (1972)"},{"key":"15_CR17","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1109\/LICS.2001.932479","volume-title":"Proceedings of the 16th IEEE Symposium on Logic in Computer Science","author":"H. Rue\u00df","year":"2001","unstructured":"Rue\u00df, H., Shankar, N.: Deconstructing Shostak. In: Proceedings of the 16th IEEE Symposium on Logic in Computer Science, pp. 19\u201328. IEEE Computer Society Press, Los Alamitos (2001)"},{"issue":"1","key":"15_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. Journal of the ACM\u00a031(1), 1\u201312 (1984)","journal-title":"Journal of the ACM"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45610-4_1","volume-title":"Rewriting Techniques and Applications","author":"N. Shankar","year":"2002","unstructured":"Shankar, N., Rue\u00df, H.: Combining Shostak theories. In: Tison, S. (ed.) RTA 2002. LNCS, vol.\u00a02378, pp. 1\u201318. Springer, Heidelberg (2002)"},{"issue":"4","key":"15_CR20","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M.E. Stickel","year":"1985","unstructured":"Stickel, M.E.: Automated deduction by theory resolution. Journal of Automated Reasoning\u00a01(4), 333\u2013355 (1985)","journal-title":"Journal of Automated Reasoning"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/10721975_16","volume-title":"Rewriting Techniques and Applications","author":"J. Stuber","year":"2000","unstructured":"Stuber, J.: Deriving theory superposition calculi from convergent term rewriting systems. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 229\u2013245. Springer, Heidelberg (2000)"},{"issue":"6","key":"15_CR22","doi-asserted-by":"publisher","first-page":"777","DOI":"10.1006\/jsco.2002.0536","volume":"33","author":"U. Waldmann","year":"2002","unstructured":"Waldmann, U.: Cancellative abelian monoids and related structures in refutational theorem proving (Part I). Journal of Symbolic Computation\u00a033(6), 777\u2013829 (2002)","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T18:12:07Z","timestamp":1559758327000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}