{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:37:45Z","timestamp":1725493065745},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540422549"},{"type":"electronic","value":"9783540457442"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45744-5_8","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T21:02:07Z","timestamp":1193432527000},"page":"92-106","source":"Crossref","is-referenced-by-count":10,"title":["The Inverse Method Implements the Automata Approach for Modal Satisfiability"],"prefix":"10.1007","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Tobies","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,8]]},"reference":[{"key":"8_CR1","volume-title":"Proc. of ECAI2000","author":"C. Areces","year":"2000","unstructured":"C. Areces, R. Gennari, J. Heguiabehere, and M. de Rijke. Tree-based heuristics in modal theorem proving. In W. Horn, editor, Proc. of ECAI2000, Berlin, Germany, 2000. IOS Press Amsterdam."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"F. Baader and U. Sattler. An overview of tableau algorithms for description logics. Studia Logica, 2001. To appear.","DOI":"10.1023\/A:1013882326814"},{"key":"8_CR3","series-title":"LTCS-Report 01-03","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45744-5_8","volume-title":"The inverse method implements the automata approach for modal satisfiability","author":"F. Baader","year":"2001","unstructured":"F. Baader and S. Tobies. The inverse method implements the automata approach for modal satisfiability. LTCS-Report 01-03, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001. See http:\/\/www-lti.informatik.rwth-aachen.de\/Forschung\/Reports.html ."},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge University Press, 2001. Publishing date May 2001, preliminary version available online from http:\/\/www.mlbook.org\/ .","DOI":"10.1017\/CBO9781107050884"},{"key":"8_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/BFb0023737","volume-title":"Proc. of Computer-Aided Verification (CAV\u2019 90)","author":"C. Courcoubetis","year":"1991","unstructured":"C. Courcoubetis, M. Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. In E. M. Clarke and R. P. Kurshan, editors, Proc. of Computer-Aided Verification (CAV\u2019 90), volume 531 of LNCS, pages 233\u2013242. Springer Verlag, 1991."},{"issue":"1","key":"8_CR6","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/S0004-3702(00)00070-9","volume":"124","author":"F. M. Donini","year":"2000","unstructured":"F. M. Donini and F. Massacci. EXPTIME tableaux for ALC. Artificial Intelligence, 124(1):87\u2013138, 2000.","journal-title":"Artificial Intelligence"},{"issue":"3","key":"8_CR7","doi-asserted-by":"publisher","first-page":"267-28","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"W. F. Dowling","year":"1984","unstructured":"W. F. Dowling and J. H. Gallier. Linear-time algorithms for testing the satisfiability of propositional horn formulae. Journal of Logic Programming, 1(3):267-28, 1984.","journal-title":"Journal of Logic Programming"},{"key":"8_CR8","series-title":"LNAI","volume-title":"Proc. of TABLEAUX 2000","year":"2000","unstructured":"R. Dyckhoff, editor. Proc. of TABLEAUX 2000, number 1847 in LNAI, St Andrews, Scotland, UK, 2000. Springer Verlag."},{"key":"8_CR9","first-page":"3","volume-title":"Proc. of the 15th International Symposium on Protocol Specification, Testing, and Verification","author":"R. Gerth","year":"1995","unstructured":"R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly Automatic verification of linear temporal logic. In Proc. of the 15th International Symposium on Protocol Specification, Testing, and Verification, pages 3\u201318, Warsaw, Poland, 1995. Chapman & Hall."},{"key":"8_CR10","volume-title":"Handbook of Tableau Methods","author":"R. Gor\u00e9","year":"1998","unstructured":"R. Gor\u00e9. Tableau methods for modal and temporal logics. In M. D\u2019Agostino, D. M. Gabbay, R. H\u00e4hnle, and J. Posegga, editors, Handbook of Tableau Methods. Kluwer, Dordrecht, 1998."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"I. Horrocks. Benchmark analysis with FaCT. In Dyckhoff[8], pages 62\u201366.","DOI":"10.1007\/10722086_6"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"U. Hustadt and R. A. Schmidt. MSPASS: Modal reasoning by translation and first-order resolution. In Dyckhoff [8], pages 67\u201371.","DOI":"10.1007\/10722086_7"},{"issue":"3","key":"8_CR13","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R. E. Ladner","year":"1977","unstructured":"R. E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing, 6(3):467\u2013480, 1977.","journal-title":"SIAM Journal on Computing"},{"key":"8_CR14","unstructured":"C. Lutz and U. Sattler. The complexity of reasoning with boolean modal logic. In Wolter F., H. Wansing, M. de Rijke, and M. Zakharyaschev, editors, Preliminary Proc. of AiML2000, Leipzig, Germany, 2000."},{"key":"8_CR15","series-title":"Lecture Notes","first-page":"189","volume-title":"Advances in Modal Logic","author":"R. A. Schmidt","year":"1998","unstructured":"R. A. Schmidt. Resolution is a decision procedure for many propositional modal logics. In M. Kracht, M. de Rijke, H. Wansing, and M. Zakharyaschev, editors, Advances in Modal Logic, Volume 1, volume 87 of Lecture Notes, pages 189\u2013208. CSLI Publications, Stanford, 1998."},{"key":"8_CR16","series-title":"PhD thesis","volume-title":"Complexity of Modal Logics","author":"E. Spaan","year":"1993","unstructured":"E. Spaan. Complexity of Modal Logics. PhD thesis, Univ. van Amsterdam, 1993."},{"key":"8_CR17","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M. Y. Vardi","year":"1986","unstructured":"M. Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Sciences, 32:183\u2013221, 1986.","journal-title":"Journal of Computer and System Sciences"},{"key":"8_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Y. Vardi","year":"1994","unstructured":"M. Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115:1\u201337, 1994.","journal-title":"Information and Computation"},{"issue":"4","key":"8_CR19","first-page":"35","volume":"1","author":"A. Voronkov","year":"2001","unstructured":"A. Voronkov. How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. ACM Transactions on Computational Logic, 1(4):35pp, 2001.","journal-title":"ACM Transactions on Computational Logic"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45744-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T01:51:14Z","timestamp":1556934674000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45744-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422549","9783540457442"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45744-5_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]}}}