{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T18:29:19Z","timestamp":1764872959884},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_22","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T03:18:26Z","timestamp":1186888706000},"page":"275-279","source":"Crossref","is-referenced-by-count":53,"title":["Spass Version 2.0"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Weidenbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uwe","family":"Brahm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Hillenbrand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enno","family":"Keen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Theobald","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dalibor","family":"Topi\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Afshordel, B., Hillenbrand, T. & Weidenbach, C. (2001), First-order atom definitions extended, in R. Nieuwenhuis & A. Voronkov, eds, \u2018Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2001\u2019, Vol. 2250 of LNAI, Springer, pp. 309\u2013319.","DOI":"10.1007\/3-540-45653-8_21"},{"key":"22_CR2","unstructured":"Antoniou, G. & Ohlbach, H. J. (1983), Terminator, in A. Bundy, ed., \u2018Proceedings of 8th International Joint Conference on Artificial Intelligence, IJCAI-83\u2019, pp. 916\u2013919."},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Bachmair, L. & Ganzinger, H. (1994), \u2018Rewrite-based equational theorem proving with selection and simplification\u2019, Journal of Logic and Computation.","DOI":"10.1093\/logcom\/4.3.217"},{"key":"22_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 4th international workshop on conditional and typed rewriting systems","author":"P. Balbiani","year":"1995","unstructured":"Balbiani, P. (1995), Equation solving in geometrical theories, in N. Dershowitz & N. Lindenstrauss, eds, \u2018Proceedings of the 4th international workshop on conditional and typed rewriting systems\u2019, Vol. 968 of LNCS, Springer."},{"key":"22_CR5","volume-title":"Geometrisches Schliessen mit Spass","author":"C. Brinker","year":"2000","unstructured":"Brinker, C. (2000), Geometrisches Schliessen mit Spass, Diplomarbeit, Universit\u00e4t des Saarlandes and Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany."},{"issue":"4","key":"22_CR6","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"P. J. Downey","year":"1980","unstructured":"Downey, P. J., Sethi, R. & Tarjan, R. E. (1980), \u2018Variations on the common subexpression problem\u2019, Journal of the ACM\n                           27(4), 758\u2013771.","journal-title":"Journal of the ACM"},{"key":"22_CR7","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/3-540-63104-6_32","volume-title":"Proceedings of the 14th International Conference on Automated Deduction, CADE-14","author":"H. Ganzinger","year":"1997","unstructured":"Ganzinger, H., Meyer, C. & Weidenbach, C. (1997), Soft typing for ordered resolution, in \u2018Proceedings of the 14th International Conference on Automated Deduction, CADE-14\u2019, Vol. 1249 of LNAI, Springer, Townsville, Australia, pp. 321\u2013335."},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Hillenbrand, T., Jaeger, A. & L\u00f6chner, B. (1999), Waldmeister-improvements in performance and ease of use, in H. Ganzinger, ed., \u201816th International Conference on Automated Deduction, CADE-16\u2019, LNAI, Springer, pp. 232\u2013236.","DOI":"10.1007\/3-540-48660-7_20"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Nonnengart, A. & Weidenbach, C. (2001), Computing small clause normal forms, in A. Robinson & A. Voronkov, eds, \u2018Handbook of Automated Reasoning\u2019, Vol. 1, Elsevier, chapter 6, pp. 335\u2013367.","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"22_CR10","volume-title":"Static analysis of list-processing C programs","author":"D. Topi\u0107","year":"2002","unstructured":"Topi\u0107, D. (2002), Static analysis of list-processing C programs, Diplomarbeit, Universit\u00e4t des Saarlandes and Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany."},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Weidenbach, C. (2001), Combining superposition, sorts and splitting, in A. Robinson & A. Voronkov, eds, \u2018Handbook of Automated Reasoning\u2019, Vol. 2, Elsevier, chapter 27, pp. 1965\u20132012.","DOI":"10.1016\/B978-044450813-3\/50029-1"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobalt, C. & Topic, D. (1999), System description: Spass version 1.0.0, in H. Ganzinger, ed., \u201816th International Conference on Automated Deduction, CADE-16\u2019, Vol. 1632 of LNAI, Springer, pp. 314\u2013318.","DOI":"10.1007\/3-540-48660-7_29"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T12:36:33Z","timestamp":1550752593000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}