{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:23Z","timestamp":1749125183589},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540613770"},{"type":"electronic","value":"9783540685074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61377-3_45","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:35:58Z","timestamp":1330292158000},"page":"308-319","source":"Crossref","is-referenced-by-count":2,"title":["On the modal logic K plus theories"],"prefix":"10.1007","author":[{"given":"Alain","family":"Heuerding","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Schwendimann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","first-page":"489","DOI":"10.1007\/BF01880326","volume":"7","author":"L. Catach","year":"1991","unstructured":"Laurent Catach. Tableaux: A general theorem prover for modal logics. Journal of Automated Reasoning, 7:489\u2013510, 1991.","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logics","author":"M. Fitting","year":"1983","unstructured":"Melvin Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, Dordrecht, 1983."},{"key":"18_CR3","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF00244394","volume":"4","author":"M. Fitting","year":"1988","unstructured":"Melvin Fitting. First-order modal tableaux. Journal of Automated Reasoning, 4:191\u2013213, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR4","volume-title":"Technical report, TR-15-95, Automated Reasoning Project","author":"R. Gor\u00e9","year":"1995","unstructured":"Rajeev Gor\u00e9. Tableau methods for modal and temporal logics. Technical report, TR-15-95, Automated Reasoning Project, Australian National University, Canberra, Australia, 1995. To appear in Handbook of Tableau Methods, Kluwer, 199?"},{"key":"18_CR5","unstructured":"Rajeev Gor\u00e9, Wolfgang Heinle, and Alain Heuerding. Relations between propositional normal modal logics: an overview. Submitted."},{"key":"18_CR6","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","volume":"54","author":"J. Y. Halpern","year":"1992","unstructured":"Joseph Y. Halpern and Yoram Moses. A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54:319\u2013379, 1992.","journal-title":"Artificial Intelligence"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Alain Heuerding, Gerhard J\u00e4ger, Stefan Schwendimann, and Michael Seyfried. Propositional logics on the computer. In Theorem Proving with Analytic Tableaux and Related Methods, LNCS 918, 1995.","DOI":"10.1007\/3-540-59338-1_44"},{"issue":"3","key":"18_CR8","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R. E. Ladner","year":"1977","unstructured":"Richard 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":"18_CR9","unstructured":"Ilkka Niemel\u00e4 and Heikki Tuominen. Helsinki logic machine: A system for logical expertise. Technical report, Digital Systems Laboratory, Department of Computer Science, Helsinki University of Technology, 1987."},{"key":"18_CR10","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/BF00244513","volume":"4","author":"F. Oppacher","year":"1988","unstructured":"F. Oppacher and E. Suen. Harp: A tableau-based theorem prover. Journal of Automated Reasoning, 4:69\u2013100, 1988.","journal-title":"Journal of Automated Reasoning"},{"issue":"5","key":"18_CR11","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1093\/logcom\/2.5.619","volume":"2","author":"D. Sahlin","year":"1992","unstructured":"Dan Sahlin, Torkel Franz\u00e9n, and Seif Haridi. An intuitionistic predicate logic theorem prover. Journal of Logic and Computation, 2(5):619\u2013656, 1992.","journal-title":"Journal of Logic and Computation"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Kurt Sch\u00fctte. Vollst\u00e4ndige Systeme modaler und intuitionistischer Logik. Springer, 1968.","DOI":"10.1007\/978-3-642-88664-5"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Alasdair Urquhart. Complexity of proofs in classical propositional logic. In Yiannis N. Moschovakis, editor, Logic from Computer Science, pages 597\u2013608. Springer, 1992.","DOI":"10.1007\/978-1-4612-2822-6_22"},{"key":"18_CR14","volume-title":"Automated Proof Search in Non-Classical Logics","author":"L. Wallen","year":"1990","unstructured":"Lincoln Wallen. Automated Proof Search in Non-Classical Logics. M.I.T. Press, Cambridge, Massachusetts, 1990."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61377-3_45.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:05:52Z","timestamp":1605647152000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61377-3_45"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540613770","9783540685074"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-61377-3_45","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}