{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T02:01:28Z","timestamp":1743127288486,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319669014"},{"type":"electronic","value":"9783319669021"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66902-1_14","type":"book-chapter","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T07:34:20Z","timestamp":1503992060000},"page":"228-244","source":"Crossref","is-referenced-by-count":1,"title":["Rule Refinement for Semantic Tableau Calculi"],"prefix":"10.1007","author":[{"given":"Dmitry","family":"Tishkovsky","sequence":"first","affiliation":[]},{"given":"Renate A.","family":"Schmidt","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,30]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/j.entcs.2009.02.029","volume":"231","author":"P Abate","year":"2009","unstructured":"Abate, P., Gor\u00e9, R.: The tableau workbench. Electr. Notes Theoret. Comput. Sci. 231, 55\u201367 (2009)","journal-title":"Electr. Notes Theoret. Comput. Sci."},{"key":"14_CR2","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/j.entcs.2010.04.003","volume":"262","author":"S Babenyshev","year":"2010","unstructured":"Babenyshev, S., Rybakov, V., Schmidt, R.A., Tishkovsky, D.: A tableau method for checking rule admissibility in S4. Electr. Notes Theoret. Comput. Sci. 262, 17\u201332 (2010)","journal-title":"Electr. Notes Theoret. Comput. Sci."},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-61630-6_1","volume-title":"Logics in Artificial Intelligence","author":"P Baumgartner","year":"1996","unstructured":"Baumgartner, P., Furbach, U., Niemel\u00e4, I.: Hyper tableaux. In: Alferes, J.J., Pereira, L.M., Orlowska, E. (eds.) JELIA 1996. LNCS, vol. 1126, pp. 1\u201317. Springer, Heidelberg (1996). doi: 10.1007\/3-540-61630-6_1"},{"key":"14_CR4","unstructured":"Baumgartner, P., Schmidt, R.A.: Blocking and other enhancements for bottom-up model generation methods (2016). arXiv e-Print arXiv:1611.09014 [cs.AI]"},{"key":"14_CR5","unstructured":"Blackburn, P., Seligman, J.: What are hybrid languages? In: AiML-1, pp. 41\u201362. CSLI Publ. (1998)"},{"issue":"3","key":"14_CR6","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1093\/logcom\/4.3.285","volume":"4","author":"M D\u2019Agostino","year":"1994","unstructured":"D\u2019Agostino, M., Mondadori, M.: The taming of the cut. Classical refutations with analytic cut. J. Log. Comput. 4(3), 285\u2013319 (1994)","journal-title":"J. Log. Comput."},{"issue":"3","key":"14_CR7","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1093\/jigpal\/8.3.265","volume":"8","author":"H Nivelle De","year":"2000","unstructured":"De Nivelle, H., Schmidt, R.A., Hustadt, U.: Resolution-based methods for modal logics. Logic J. IGPL 8(3), 265\u2013292 (2000)","journal-title":"Logic J. IGPL"},{"key":"14_CR8","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":"Fitting, M.: Proof Methods for Modal and Intuitionistic Logics. Reidel, Kufstein (1983)"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Gargov, G., Passy, S., Tinchev, T.: Modal environment for Boolean speculations. In: Proceedings of the 1986 G\u00f6del Conference, pp. 253\u2013263. Plenum (1987)","DOI":"10.1007\/978-1-4613-0897-3_17"},{"key":"14_CR10","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-94-017-1754-0_6","volume-title":"Handbook of Tableau Methods","author":"R Gor\u00e9","year":"1999","unstructured":"Gor\u00e9, R.: Tableau methods for modal and temporal logics. In: D\u2019Agostino, M., Gabbay, D.M., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 297\u2013396. Springer, Dordrecht (1999). doi: 10.1007\/978-94-017-1754-0_6"},{"issue":"6","key":"14_CR11","doi-asserted-by":"crossref","first-page":"819","DOI":"10.1093\/logcom\/6.6.819","volume":"6","author":"R H\u00e4hnle","year":"1996","unstructured":"H\u00e4hnle, R., Klingenbeck, S.: A-ordered tableaux. J. Log. Comput. 6(6), 819\u2013833 (1996)","journal-title":"J. Log. Comput."},{"issue":"2","key":"14_CR12","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1305\/ndjfl\/1093636937","volume":"28","author":"IL Humberstone","year":"1987","unstructured":"Humberstone, I.L.: The modal logic of \u2018all and only\u2019. Notre Dame J. Formal Log. 28(2), 177\u2013188 (1987)","journal-title":"Notre Dame J. Formal Log."},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-69778-0_22","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"U Hustadt","year":"1998","unstructured":"Hustadt, U., Schmidt, R.A.: Simplification and backjumping in modal tableau. In: Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 187\u2013201. Springer, Heidelberg (1998). doi: 10.1007\/3-540-69778-0_22"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-40537-2_17","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M Khodadadi","year":"2013","unstructured":"Khodadadi, M., Schmidt, R.A., Tishkovsky, D.: A refined tableau calculus with controlled blocking for the description logic $$\\cal{SHOI}$$ SHOI . In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS, vol. 8123, pp. 188\u2013202. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40537-2_17"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Lutz, C., Sattler, U.: The complexity of reasoning with Boolean modal logics. In: AiML-3, pp. 329\u2013348. CSLI Publ. (2002)","DOI":"10.1142\/9789812776471_0018"},{"key":"14_CR16","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1613\/jair.2811","volume":"36","author":"B Motik","year":"2009","unstructured":"Motik, B., Shearer, R., Horrocks, I.: Hypertableau reasoning for description logics. J. Artif. Intell. Res. 36, 165\u2013228 (2009)","journal-title":"J. Artif. Intell. Res."},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning, pp. 335\u2013367. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"14_CR18","unstructured":"Schmidt, R.A., Stell, J.G., Rydeheard, D.: Axiomatic and tableau-based reasoning for Kt(H, R). In: AiML-10, pp. 478\u2013497. College Publ. (2014)"},{"issue":"2:6","key":"14_CR19","first-page":"1","volume":"7","author":"RA Schmidt","year":"2011","unstructured":"Schmidt, R.A., Tishkovsky, D.: Automated synthesis of tableau calculi. Log. Methods Comput. Sci. 7(2:6), 1\u201332 (2011)","journal-title":"Log. Methods Comput. Sci."},{"issue":"1","key":"14_CR20","doi-asserted-by":"crossref","first-page":"7:1","DOI":"10.1145\/2559947","volume":"15","author":"RA Schmidt","year":"2014","unstructured":"Schmidt, R.A., Tishkovsky, D.: Using tableau to decide description logics with full role negation and identity. ACM Trans. Comput. Log. 15(1), 7:1\u20137:31 (2014)","journal-title":"ACM Trans. Comput. Log."},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-319-24312-2_4","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"RA Schmidt","year":"2015","unstructured":"Schmidt, R.A., Waldmann, U.: Modal tableau systems with blocking and congruence closure. In: Nivelle, H. (ed.) TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 38\u201353. Springer, Cham (2015). doi: 10.1007\/978-3-319-24312-2_4"},{"key":"14_CR22","volume-title":"First Order Logic","author":"RM Smullyan","year":"1971","unstructured":"Smullyan, R.M.: First Order Logic. Springer, Heidelberg (1971)"},{"issue":"4","key":"14_CR23","doi-asserted-by":"crossref","first-page":"500","DOI":"10.1016\/j.jlamp.2015.11.003","volume":"85","author":"JG Stell","year":"2016","unstructured":"Stell, J.G., Schmidt, R.A., Rydeheard, D.: A bi-intuitionistic modal logic: foundations and automation. J. Log. Algebr. Methods Program. 85(4), 500\u2013519 (2016)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"14_CR24","unstructured":"Tishkovsky, D., Schmidt, R.A.: Rule refinement for semantic tableau calculi (2017). http:\/\/www.cs.man.ac.uk\/~schmidt\/publications\/ruleref_long.pdf"}],"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\/978-3-319-66902-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T17:55:31Z","timestamp":1570038931000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66902-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319669014","9783319669021"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66902-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}