{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:20:40Z","timestamp":1758979240365},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_38","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T05:31:33Z","timestamp":1188451893000},"page":"514-520","source":"Crossref","is-referenced-by-count":43,"title":["System Description: Spass Version 3.0"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Weidenbach","sequence":"first","affiliation":[]},{"given":"Renate A.","family":"Schmidt","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Hillenbrand","sequence":"additional","affiliation":[]},{"given":"Rostislav","family":"Rusev","sequence":"additional","affiliation":[]},{"given":"Dalibor","family":"Topic","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"38_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/11814771_11","volume-title":"Automated Reasoning","author":"P. Baumgartner","year":"2006","unstructured":"Baumgartner, P., Schmidt, R.A.: Blocking and other enhancements for bottom-up model generation methods. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 125\u2013139. Springer, Heidelberg (2006)"},{"key":"38_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/10722086_7","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"U. Hustadt","year":"2000","unstructured":"Hustadt, U., Schmidt, R.A.: MSPASS: Modal reasoning by translation and first-order resolution. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol.\u00a01847, pp. 67\u201371. Springer, Heidelberg (2000)"},{"key":"38_CR3","first-page":"251","volume":"1","author":"U. Hustadt","year":"2004","unstructured":"Hustadt, U., Schmidt, R.A., Georgieva, L.: A survey of decidable first-order fragments and description logics. J. Relational Meth. in Computer Sci.\u00a01, 251\u2013276 (2004)","journal-title":"J. Relational Meth. in Computer Sci."},{"key":"38_CR4","unstructured":"Hustadt, U., Schmidt, R.A., Weidenbach, C., MSPASS,: Subsumption testing with SPASS. In: Proc. DL 1999, pp. 136\u2013137. Link\u00f6ping University (1999)"},{"key":"38_CR5","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/B978-044450813-3\/50008-4","volume-title":"Handbook of Automated Reasoning","author":"A. Nonnengart","year":"2001","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning, pp. 335\u2013367. Elsevier, Amsterdam (2001)"},{"key":"38_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/11828563","volume-title":"Volume in memoriam of Harald Ganzinger","author":"R.A. Schmidt","year":"2006","unstructured":"Schmidt, R.A., Hustadt, U.: First-order resolution methods for modal logics. In: Volume in memoriam of Harald Ganzinger, Springer. LNCS, Springer, Heidelberg (2006), \n                    \n                      http:\/\/www.cs.man.ac.uk\/~schmidt\/publications\/SchmidtHustadt06a.html"},{"key":"38_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/3-540-45620-1_22","volume-title":"Automated Deduction - CADE-18","author":"C. Weidenbach","year":"2002","unstructured":"Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., Topic, D.: SPASS version 2.0. In: Voronkov, A. (ed.) Automated Deduction - CADE-18. LNCS (LNAI), vol.\u00a02392, pp. 275\u2013279. Springer, Heidelberg (2002)"},{"key":"38_CR8","unstructured":"Weidenbach, C., Schmidt, R.A., Keen, E.: SPASS handbook version 3.0. Contained in the distribution of SPASS Version 3.0 (2007)"},{"key":"38_CR9","unstructured":"Weidenbach, C., Schmidt, R.A., Topic, D.: SPASS input syntax version 3.0. Contained in the distribution of SPASS Version 3.0 (2007)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_38.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T05:53:11Z","timestamp":1619502791000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}