{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:21Z","timestamp":1749125181977},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615118"},{"type":"electronic","value":"9783540686873"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_75","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:49:55Z","timestamp":1330292995000},"page":"141-145","source":"Crossref","is-referenced-by-count":42,"title":["SPASS & FLOTTER version 0.42"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Weidenbach","sequence":"first","affiliation":[]},{"given":"Bernd","family":"Gaede","sequence":"additional","affiliation":[]},{"given":"Georg","family":"Rock","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"issue":"3","key":"12_CR1","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217\u2013247, 1994.","journal-title":"Journal of Logic and Computation"},{"key":"12_CR2","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1016\/0747-7171(92)90009-S","volume":"14","author":"T. B. Tour de la","year":"1992","unstructured":"Thierry Boy de la Tour. An optimality result for clause form translation. Journal of Symbolic Computation, 14:283\u2013301, 1992.","journal-title":"Journal of Symbolic Computation"},{"key":"12_CR3","first-page":"1","volume":"27","author":"L. Dafa","year":"1994","unstructured":"Li Dafa. The Formulation of the Halting Problem is Not Suitable for Describing the Halting Problem. Association for Automated Reasoning Newsletter, 27:1\u20137, October 1994.","journal-title":"Association for Automated Reasoning Newsletter"},{"doi-asserted-by":"crossref","unstructured":"Peter Graf. Substitution tree indexing. In Rewriting Techniques and Applications, RTA-95, volume 914 of LNCS, pages 117\u2013131. Springer, 1995.","key":"12_CR4","DOI":"10.1007\/3-540-59200-8_52"},{"doi-asserted-by":"crossref","unstructured":"William McCune. Otter 2.0. In 10th International Conference on Automated Deduction, CADE-10, volume 449 of LNCS, pages 663\u2013664. Springer, 1990.","key":"12_CR5","DOI":"10.1007\/3-540-52885-7_131"},{"issue":"3","key":"12_CR6","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/BF00244274","volume":"1","author":"H. Ohlbach","year":"1985","unstructured":"Hans-J\u00fcrgen Ohlbach and Manfred Schmidt-Schau\u00df. The lion and the unicorn. Journal of Automated Reasoning, 1(3):327\u2013332, 1985.","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"12_CR7","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/BF00881919","volume":"15","author":"H. Ohlbach","year":"1995","unstructured":"Hans-J\u00fcrgen Ohlbach and Christoph Weidenbach. A note on assumptions about skolem functions. Journal of Automated Reasoning, 15(2):267\u2013275, 1995.","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"12_CR8","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F. J. Pelletier","year":"1986","unstructured":"Francis Jeffry Pelletier. Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning, 2(2):191\u2013216, 1986. Errata: Journal of Automated Reasoning, 4(2):235\u2013236,1988.","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR9","first-page":"8","volume":"31","author":"F. J. Pelletier","year":"1995","unstructured":"Francis Jeffry Pelletier and Geoff Sutcliffe. An Erratum for Some Errata to Automated Theorem Proving Problems. Association for Automated Reasoning Newsletter, 31:8\u201314, December 1995.","journal-title":"Association for Automated Reasoning Newsletter"},{"issue":"1","key":"12_CR10","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G.E. Peterson","year":"1983","unstructured":"G.E. Peterson. A technique for establishing completeness results in theorem proving with equality. SIAM Journal of Computation, 12(1):82\u2013100, February 1983.","journal-title":"SIAM Journal of Computation"},{"key":"12_CR11","volume-title":"Master's thesis","author":"G. Rock","year":"1995","unstructured":"Georg Rock. Transformations of first-order formulae for automated reasoning. Master's thesis, Max-Planck-Institut f\u00fcr Informatik, Germany, April 1995. Supervisors: H.J. Ohlbach, C. Weidenbach."},{"key":"12_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(91)90078-X","volume":"48","author":"M. Schmidt-Schau\u00df","year":"1991","unstructured":"Manfred Schmidt-Schau\u00df and Gerd Smolka. Attributive concept description with complements. Artificial Intelligence, 48:1\u201326, 1991.","journal-title":"Artificial Intelligence"},{"issue":"1","key":"12_CR13","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/BF00246025","volume":"2","author":"M. Stickel","year":"1986","unstructured":"Mark Stickel. Schubert's steamroller problem: Formulations and solutions. Journal of Automated Reasoning, 2(1):89\u2013101, 1986.","journal-title":"Journal of Automated Reasoning"},{"unstructured":"Christoph Weidenbach. Extending the resolution method with sorts. In Proc. of 13th International Joint Conference on Artificial Intelligence, IJCAI-93, pages 60\u201365. Morgan Kaufmann, 1993.","key":"12_CR14"},{"issue":"6","key":"12_CR15","first-page":"887","volume":"3","author":"C. Weidenbach","year":"1995","unstructured":"Christoph Weidenbach. First-order tableaux with sorts. Journal of the Interest Group in Pure and Applied Logics, IGPL, 3(6):887\u2013906, 1995.","journal-title":"Journal of the Interest Group in Pure and Applied Logics, IGPL"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_75.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:33:40Z","timestamp":1619573620000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_75"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_75","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}