{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T06:17:23Z","timestamp":1784873843121,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642029585","type":"print"},{"value":"9783642029592","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02959-2_10","type":"book-chapter","created":{"date-parts":[[2009,7,25]],"date-time":"2009-07-25T05:02:22Z","timestamp":1248498142000},"page":"140-145","source":"Crossref","is-referenced-by-count":156,"title":["SPASS Version 3.5"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Weidenbach","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dilyana","family":"Dimova","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Arnaud","family":"Fietzke","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rohit","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Suda","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Patrick","family":"Wischnewski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"3","key":"10_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); Revised version of Max-Planck-Institut f\u00fcr Informatik technical report, MPI-I-91-208 (1991)","journal-title":"Journal of Logic and Computation"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-540-71070-7_39","volume-title":"Automated Reasoning","author":"A. Fietzke","year":"2008","unstructured":"Fietzke, A., Weidenbach, C.: Labelled splitting. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol.\u00a05195, pp. 459\u2013474. Springer, Heidelberg (2008)"},{"key":"10_CR3","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/3-540-63104-6_32","volume-title":"Automated Deduction - CADE-14","author":"H. Ganzinger","year":"1997","unstructured":"Ganzinger, H., Meyer, C., Weidenbach, C.: Soft typing for ordered resolution. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol.\u00a01249, pp. 321\u2013335. Springer, Heidelberg (1997)"},{"key":"10_CR4","unstructured":"Ganzinger, H., Nieuwenhuis, R.: The saturate system 1994 (1994), \n                    \n                      http:\/\/www.mpi-sb.mpg.de\/SATURATE\/Saturate.html"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/3-540-56393-8_17","volume-title":"Conditional Term Rewriting Systems","author":"H. Ganzinger","year":"1992","unstructured":"Ganzinger, H., Stuber, J.: Inductive theorem proving by consistency for first-order clauses. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol.\u00a0656, pp. 226\u2013241. Springer, Heidelberg (1992)"},{"key":"10_CR6","unstructured":"Hillenbrand, T., Weidenbach, C.: Superposition for finite domains. Research Report MPI-I-2007-RG1-002, Max-Planck Institute for Informatics, Saarbruecken, Germany (April 2007)"},{"key":"10_CR7","series-title":"LNAI","first-page":"404","volume-title":"CADE 2009","author":"M. Horbach","year":"2009","unstructured":"Horbach, M., Weidenbach, C.: Decidability results for saturation-based model building. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol.\u00a05663, pp. 404\u2013420. Springer, Heidelberg (2009)"},{"key":"10_CR8","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/B978-044450813-3\/50008-4","volume-title":"Handbook of Automated Reasoning, ch. 6","author":"A. Nonnengart","year":"2001","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 6, vol.\u00a01, pp. 335\u2013367. Elsevier, Amsterdam (2001)"},{"issue":"2","key":"10_CR9","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP problem library \u2013 cnf release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"issue":"2-4","key":"10_CR10","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/BF02127750","volume":"18","author":"C. Weidenbach","year":"1996","unstructured":"Weidenbach, C.: Unification in sort theories and its applications. Annals of Mathematics and Artificial Intelligence\u00a018(2-4), 261\u2013293 (1996)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"10_CR11","doi-asserted-by":"publisher","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning, ch. 27","author":"C. Weidenbach","year":"2001","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 27, vol.\u00a02, pp. 1965\u20132012. Elsevier, Amsterdam (2001)"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Weidenbach","year":"2007","unstructured":"Weidenbach, C., Schmidt, R., Hillenbrand, T., Rusev, R., Topic, D.: Spass version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol.\u00a04603, pp. 514\u2013520. Springer, Heidelberg (2007)"},{"key":"10_CR13","unstructured":"Weidenbach, C., Wischnewski, P.: Contextual rewriting in Spass. In: PAAR\/ESHOL, Sydney, Australien. CEUR Workshop Proceedings, vol.\u00a0373, pp. 115\u2013124 (2008)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-22"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02959-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,25]],"date-time":"2019-01-25T13:02:13Z","timestamp":1548421333000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02959-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642029585","9783642029592"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}