{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T22:29:43Z","timestamp":1791152983121,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540676973","type":"print"},{"value":"9783540450085","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722086_7","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T19:43:15Z","timestamp":1167421395000},"page":"67-71","source":"Crossref","is-referenced-by-count":32,"title":["MSPASS: Modal Reasoning by Translation and First-Order Resolution"],"prefix":"10.1007","author":[{"given":"Ullrich","family":"Hustadt","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Renate A.","family":"Schmidt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"3","key":"7_CR1","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1093\/logcom\/2.3.247","volume":"2","author":"Y. Auffray","year":"1992","unstructured":"Auffray, Y., Enjalbert, P.: Modal theorem proving: An equational viewpoint. J. Logic Computat.\u00a02(3), 247\u2013297 (1992)","journal-title":"J. Logic Computat."},{"issue":"3","key":"7_CR2","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. J. Logic Computat.\u00a04(3), 217\u2013247 (1994)","journal-title":"J. Logic Computat."},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"De Nivelle, H., Schmidt, R.A., Hustadt, U.: Resolution-based methods for modal logics. Logic J. IGPL (2000) (to appear)","DOI":"10.1093\/jigpal\/8.3.265"},{"key":"7_CR4","first-page":"295","volume-title":"Proc. LICS 1999","author":"H. Ganzinger","year":"1999","unstructured":"Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: Proc. LICS 1999, pp. 295\u2013303. IEEE Computer Soc, Los Alamitos (1999)"},{"key":"7_CR5","unstructured":"Herzig, A.: Raisonnement automatique en logique modale et algorithmes d\u2019unification. PhD thesis, Univ. Paul-Sabatier, Toulouse (1989)"},{"key":"7_CR6","unstructured":"Hustadt, U.: Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD thesis, Univ. d. Saarlandes, Saarbr\u00fccken, Germany (1999)"},{"issue":"4","key":"7_CR7","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1080\/11663081.1999.10510981","volume":"9","author":"U. Hustadt","year":"1999","unstructured":"Hustadt, U., Schmidt, R.A.: An empirical analysis of modal theorem provers. J. Appl. Non-Classical Logics\u00a09(4), 479\u2013522 (1999)","journal-title":"J. Appl. Non-Classical Logics"},{"key":"7_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-48660-7_12","volume-title":"Automated Deduction - CADE-16","author":"U. Hustadt","year":"1999","unstructured":"Hustadt, U., Schmidt, R.A.: Maslov\u2019s class K revisited. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 172\u2013186. Springer, Heidelberg (1999)"},{"key":"7_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/3-540-46508-1_13","volume-title":"Automated Deduction in Classical and Non-Classical Logics","author":"U. Hustadt","year":"2000","unstructured":"Hustadt, U., Schmidt, R.A.: Issues of decidability for description logics in the framework of resolution. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol.\u00a01761, pp. 191\u2013205. Springer, Heidelberg (2000)"},{"key":"7_CR10","unstructured":"Hustadt, U., Schmidt, R.A.: Using resolution for testing modal satisfiability and building models. To appear in J. Automated Reasoning (2000)"},{"key":"7_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/3-540-69778-0_9","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"U. Hustadt","year":"1998","unstructured":"Hustadt, U., Schmidt, R.A., Weidenbach, C.: Optimised functional translation and resolution. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, pp. 36\u201337. Springer, Heidelberg (1998)"},{"key":"7_CR12","first-page":"80","volume-title":"Proc. IJCAI 1993","author":"A. Nonnengart","year":"1993","unstructured":"Nonnengart, A.: First-order modal logic theorem proving and functional simulation. In: Proc. IJCAI 1993, pp. 80\u201385. Morgan Kaufmann, San Francisco (1993)"},{"key":"7_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/BFb0054274","volume-title":"Automated Deduction - CADE-15","author":"A. Nonnengart","year":"1998","unstructured":"Nonnengart, A., Rock, G., Weidenbach, C.: On generating small clause normal forms. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 397\u2013411. Springer, Heidelberg (1998)"},{"issue":"5","key":"7_CR14","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1093\/logcom\/1.5.691","volume":"1","author":"H.J. Ohlbach","year":"1991","unstructured":"Ohlbach, H.J.: Semantics based translation methods for modal logics. J. Logic Computat.\u00a01(5), 691\u2013746 (1991)","journal-title":"J. Logic Computat."},{"issue":"5","key":"7_CR15","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1093\/logcom\/7.5.581","volume":"7","author":"H.J. Ohlbach","year":"1997","unstructured":"Ohlbach, H.J., Schmidt, R.A.: Functional translation and second-order frame properties of modal logics. J. Logic Computat.\u00a07(5), 581\u2013603 (1997)","journal-title":"J. Logic Computat."},{"issue":"4","key":"7_CR16","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1023\/A:1006043519663","volume":"22","author":"R.A. Schmidt","year":"1999","unstructured":"Schmidt, R.A.: Decidability by resolution for propositional modal logics. J. Automated Reasoning\u00a022(4), 379\u2013396 (1999)","journal-title":"J. Automated Reasoning"},{"key":"7_CR17","unstructured":"Schmidt, R.A.: MSPASS (1999), \n                    \n                      http:\/\/www.cs.man.ac.uk\/~schmidt\/mspass\/"},{"issue":"1","key":"7_CR18","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1023\/A:1006006930186","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The CADE-14 ATP system competition. J. Automated Reasoning\u00a021(1), 99\u2013134 (1998)","journal-title":"J. Automated Reasoning"},{"key":"7_CR19","unstructured":"Weidenbach, C.: SPASS (1999), \n                    \n                      http:\/\/spass.mpi-sb.mpg.de"},{"key":"7_CR20","volume-title":"Handbook of Automated Reasoning","author":"C. Weidenbach","year":"2000","unstructured":"Weidenbach, C.: SPASS: Combining superposition, sorts and splitting. In: Handbook of Automated Reasoning. Elsevier, Amsterdam (2000) (to appear)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722086_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T05:32:47Z","timestamp":1553319167000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722086_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676973","9783540450085"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/10722086_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000]]}}}