{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:29:01Z","timestamp":1725568141273},"publisher-location":"Berlin, Heidelberg","reference-count":20,"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_31","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"335-349","source":"Crossref","is-referenced-by-count":8,"title":["Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation"],"prefix":"10.1007","author":[{"given":"Harald","family":"Ganzinger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Stuber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"31_CR1","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BF00881838","volume":"10","author":"A. Avron","year":"1993","unstructured":"Avron, A.: Gentzen-type systems, resolution and tableaux. Journal of Automated Reasoning\u00a010(2), 265\u2013281 (1993)","journal-title":"Journal of Automated Reasoning"},{"key":"31_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/BFb0013068","volume-title":"Logic Programming and Automated Reasoning","author":"L. Bachmair","year":"1992","unstructured":"Bachmair, L., Ganzinger, H.: Non-clausal resolution and superposition with selection and redundancy criteria. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 273\u2013284. Springer, Heidelberg (1992)"},{"key":"31_CR3","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Conditional and Typed Rewriting Systems","author":"L. Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H.: Associative-commutative superposition. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol.\u00a0968, pp. 1\u201314. Springer, Heidelberg (1995)"},{"key":"31_CR4","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning","author":"L. Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, ch. 2, pp. 19\u2013100. North Holland, Amsterdam (2001)"},{"issue":"2","key":"31_CR5","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L. Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation. Information and Computation\u00a0121(2), 172\u2013192 (1995)","journal-title":"Information and Computation"},{"key":"31_CR6","unstructured":"The CADE-18 ATP System Competition (CASC-18) (2002), http:\/\/www.cs.miami.edu\/~tptp\/CASC\/18\/"},{"key":"31_CR7","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/10721959_28","volume-title":"Automated Deduction - CADE-17","author":"A. Degtyarev","year":"2000","unstructured":"Degtyarev, A., Voronkov, A.: Stratified resolution. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol.\u00a01831, pp. 365\u2013384. Springer, Heidelberg (2000)"},{"key":"31_CR8","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Rapport de Recherche 3400, INRIA (1998)"},{"key":"31_CR9","unstructured":"Ganzinger, H., Nieuwenhuis, R., Nivela, P.: The Saturate system (1994), System available at http:\/\/www.mpi-sb.mpg.de\/SATURATE\/"},{"key":"31_CR10","unstructured":"Huet, G.: The zipper talk. Invited Lecture at FLoC 1996 (1996)"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Transactions on Programming Languages and Systems\u00a02(1) (1980)","DOI":"10.1145\/357084.357090"},{"issue":"1","key":"31_CR12","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0004-3702(82)90011-X","volume":"18","author":"N.V. Murray","year":"1982","unstructured":"Murray, N.V.: Completely non-clausal theorem proving. Artificial Intelligence\u00a018(1), 67\u201385 (1982)","journal-title":"Artificial Intelligence"},{"key":"31_CR13","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R. Nieuwenhuis","year":"1995","unstructured":"Nieuwenhuis, R., Rubio, A.: Theorem proving with ordering and equality constrained clauses. Journal of Symbolic Computation\u00a019, 321\u2013351 (1995)","journal-title":"Journal of Symbolic Computation"},{"key":"31_CR14","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, ch. 7, pp. 371\u2013443. North Holland, Amsterdam (2001)"},{"key":"31_CR15","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Communications\u00a015(2-3) (2002)"},{"key":"31_CR16","unstructured":"Schulz, S.: E-Setheo, http:\/\/www4.informatik.tu-muenchen.de\/~schulz\/WORK\/e-setheo.html"},{"key":"31_CR17","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)"},{"key":"31_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/3-540-45744-5_15","volume-title":"Automated Reasoning","author":"J. Stuber","year":"2001","unstructured":"Stuber, J.: A model-based completeness proof of Extended Narrowing And Resolution. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 195\u2013210. Springer, Heidelberg (2001)"},{"key":"#cr-split#-31_CR19.1","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus (1970);","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"#cr-split#-31_CR19.2","doi-asserted-by":"crossref","unstructured":"Reprinted in Siekmann, J., Wrightson, G. (eds) Automation of Reasoning, vol. 2, pp. 466???486. Springer, Heidelberg (1983)","DOI":"10.1007\/978-3-642-81955-1"}],"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_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T22:12:04Z","timestamp":1559772724000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}