{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T15:05:37Z","timestamp":1747580737836},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_35","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T20:53:07Z","timestamp":1194641587000},"page":"383-387","source":"Crossref","is-referenced-by-count":3,"title":["K : A Theorem Prover for K"],"prefix":"10.1007","author":[{"given":"Andrei","family":"Voronkov","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"F. Baader and B. Hollunder. A terminological knowledge representation system with complete inference algorithms. In H. Boley and M.M. Richter, editors, Processing Declarative Knowledge (Proceedings of the International Workshop PDK\u201991, volume 567 of Lecture Notes in Artificial Intelligence, pages 67\u201386. Springer Verlag, 1991.","key":"35_CR1","DOI":"10.1007\/BFb0013522"},{"issue":"4","key":"35_CR2","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/BF01880326","volume":"7","author":"L. Catach","year":"1991","unstructured":"L. Catach. Tableaux: a general theorem prover for modal logics. Journal of Automated Reasoning, 7(4):489\u2013510, 1991.","journal-title":"Journal of Automated Reasoning"},{"key":"35_CR3","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/BF00156916","volume":"1","author":"M. D\u2019Agostino","year":"1992","unstructured":"M. D\u2019Agostino. Are tableaux an improvement of truth tables? Journal of Logic, Language and Information, 1:235\u2013252, 1992.","journal-title":"Journal of Logic, Language and Information"},{"key":"35_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1007\/3-540-61511-3_115","volume-title":"CADE-13","author":"F. Giunchiglia","year":"1996","unstructured":"F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures: Case study of modal K. In M.A. McRobbie and J.K. Slaney, editors, CADE-13, volume 1104 of Lecture Notes in Computer Science, pages 583\u2013597, 1996."},{"key":"35_CR5","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1305\/ndjfl\/1093891406","volume":"15","author":"L.F. Goble","year":"1974","unstructured":"L.F. Goble. Gentzen systems for modal logic. Notre Dame J. of Formal Logic, 15:455\u2013461, 1974.","journal-title":"Notre Dame J. of Formal Logic"},{"key":"35_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/3-540-69778-0_5","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX\u201998","author":"I. Horrocks","year":"1998","unstructured":"I. Horrocks and P.F. Patel-Schneider. FaCT and DLP. In H. de Swart, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX\u201998, volume 1397 of Lecture Notes in Computer Science, pages 27\u201330, Oisterwijk, The Netherlands, May 1998. Springer Verlag."},{"doi-asserted-by":"crossref","unstructured":"I. Horrocks and P.F. Patel-Schneider. Optimising description logic subsumption. Journal of Logic and Computation, 1999. To appear.","key":"35_CR7","DOI":"10.1093\/logcom\/9.3.267"},{"key":"35_CR8","first-page":"202","volume":"1","author":"U. Hustadt","year":"1997","unstructured":"U. Hustadt and R. Schmidt. On evaluating decision procedures for modal logic. In IJCAI-97, volume 1, pages 202\u2013207, 1997.","journal-title":"IJCAI-97"},{"key":"35_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/3-540-69778-0_22","volume-title":"TABLEAUX\u201998","author":"U. Hustadt","year":"1998","unstructured":"U. Hustadt and R.A. Schmidt. Simplification and backjumping in modal tableau. In H. de Swart, editor, TABLEAUX\u201998, volume 1397 of Lecture Notes in Computer Science, pages 187\u2013201, 1998."},{"unstructured":"U. Hustadt and R.A. Schmidt. On the relation of resolution and tableaux proof systems for description logics. In IJCAI-99, 1999. To appear.","key":"35_CR10"},{"doi-asserted-by":"crossref","unstructured":"S. Yu. Maslov. An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning (Classical papers on Computational Logic), volume 2, pages 48\u201354. Springer Verlag, 1983.","key":"35_CR11","DOI":"10.1007\/978-3-642-81955-1_3"},{"doi-asserted-by":"crossref","unstructured":"A. Voronkov. Theorem proving in non-standard logics based on the inverse method. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 648\u2013662, 1992.","key":"35_CR12","DOI":"10.1007\/3-540-55602-8_198"},{"unstructured":"A. Voronkov. A bottom-up decision procedure for propositional K: theory and implementation. 1999. To be submitted.","key":"35_CR13"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T08:56:35Z","timestamp":1556960195000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_35","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}