{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:35:06Z","timestamp":1753889706576,"version":"3.41.2"},"reference-count":37,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,5,7]],"date-time":"2011-05-07T00:00:00Z","timestamp":1304726400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>This paper presents a method for synthesising sound and complete tableau\ncalculi. Given a specification of the formal semantics of a logic, the method\ngenerates a set of tableau inference rules that can then be used to reason\nwithin the logic. The method guarantees that the generated rules form a\ncalculus which is sound and constructively complete. If the logic can be shown\nto admit finite filtration with respect to a well-defined first-order semantics\nthen adding a general blocking mechanism provides a terminating tableau\ncalculus. The process of generating tableau rules can be completely automated\nand produces, together with the blocking mechanism, an automated procedure for\ngenerating tableau decision procedures. For illustration we show the\nworkability of the approach for a description logic with transitive roles and\npropositional intuitionistic logic.<\/jats:p>","DOI":"10.2168\/lmcs-7(2:6)2011","type":"journal-article","created":{"date-parts":[[2011,9,23]],"date-time":"2011-09-23T12:17:26Z","timestamp":1316780246000},"source":"Crossref","is-referenced-by-count":14,"title":["Automated Synthesis of Tableau Calculi"],"prefix":"10.46298","volume":"Volume 7, Issue 2","author":[{"given":"Renate A.","family":"Schmidt","sequence":"first","affiliation":[]},{"given":"Dmitry","family":"Tishkovsky","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2011,5,7]]},"reference":[{"key":"10.2168\/LMCS-7(2:6)2011_AbateGore03","unstructured":"P. Abate and R. Gor\u00e9. The Tableaux Work Bench. In M. C. Mayer and F. Pirri, eds,Proceedings of the 12th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'03), vol. 2796 ofLecture Notes in Computer Science, pp. 230-236. Springer, 2003."},{"key":"10.2168\/LMCS-7(2:6)2011_DBLP:conf\/csl\/AlendaOST10","unstructured":"R. Alenda, N. Olivetti, C. Schwind, and D. Tishkovsky. Tableau calculi for CSL over minspaces. In A. Dawar and H. Veith, eds,Proceedings of the 19th Annual Conference of the European Association for Computer Science Logic (CSL'10), vol. 6247 ofLecture Notes in Computer Science, pp. 52-66. Springer, 2010."},{"key":"10.2168\/LMCS-7(2:6)2011_AvelloneEtAl97","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0027404"},{"key":"10.2168\/LMCS-7(2:6)2011_BaaderCalvaneseEtal03","unstructured":"F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, and P. F. Patel-Schneider.Description Logic Handbook. Cambridge University Press, 2003."},{"key":"10.2168\/LMCS-7(2:6)2011_BaaderSattler01","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1013882326814","volume":"69","author":"F. Baader and U. Sattler","year":"2001","journal-title":"Studia Logica"},{"issue":"1","key":"10.2168\/LMCS-7(2:6)2011_BalbianiEtAl10","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1093\/logcom\/exn060","volume":"20","author":"P. Balbiani, H. P. van Ditmarsch, A. Her","year":"2010","journal-title":"Journal of Logic and Computation"},{"key":"10.2168\/LMCS-7(2:6)2011_BaumgartnerSchmidt06","unstructured":"P. Baumgartner and R. A. Schmidt. Blocking and other enhancements for bottom-up model generation methods. In U. Furbach and N. Shankar, eds,Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06), vol. 4130 ofLecture Notes in Artificial Intelligence, pp. 125-139. Springer, 2006."},{"key":"10.2168\/LMCS-7(2:6)2011_BlackburnDeRijkeVenema01","doi-asserted-by":"crossref","unstructured":"P. Blackburn, M. de Rijke, and V. Venema.Modal Logic. Cambridge University Press, 2001.","DOI":"10.1017\/CBO9781107050884"},{"key":"10.2168\/LMCS-7(2:6)2011_Blackburn-WHL-1998","unstructured":"P. Blackburn and J. Seligman. What are hybrid languages? In M. Kracht, M. de Rijke, H. Wansing, and M. Zakharyaschev, eds,Advances in Modal Logic, Volume 1, pp. 41-62. CSLI Publications, 1998."},{"issue":"3","key":"10.2168\/LMCS-7(2:6)2011_BolanderBlackburn07","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1093\/logcom\/exm014","volume":"17","author":"T. Bolander and P. Blackburn","year":"2007","journal-title":"Journal of Logic and Computation"},{"key":"10.2168\/LMCS-7(2:6)2011_BryManthey87","doi-asserted-by":"crossref","unstructured":"F. Bry and R. Manthey. Proving finite satisfiability of deductive databases. In E. B\u00f6rger, H. Kleine B\u00fcning, and M. M. Richter, eds,Proceedings of the 1st Workshop on Computer Science Logic (CSL'87), vol. 329 ofLecture Notes in Computer Science, pp. 44-55. Springer, 1988.","DOI":"10.1007\/3-540-50241-6_28"},{"key":"10.2168\/LMCS-7(2:6)2011_BryTorge98","unstructured":"F. Bry and S. Torge. A deduction method complete for refutation and finite satisfiability. In J. Dix, L. Fari\u00f1as del Cerro, and U. Furbach, eds,Proceedings of the 6th European Conference on Logics in Artificial Intelligence (JELIA'98), vol. 1489 ofLecture Notes in Computer Science, pp. 1-17. Springer, 1998."},{"issue":"32","key":"10.2168\/LMCS-7(2:6)2011_CastilhoFarinasDelCerroGasquetHerzig97","first-page":"281","volume":"4","author":"M. A. Castilho, L. Fari\u00f1as del Cerro, O.","year":"1997","journal-title":"Fundamenta Informaticae"},{"key":"10.2168\/LMCS-7(2:6)2011_CialdeaMayerCerrito01","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1023\/A:1013838528631","volume":"69","author":"M. Cialdea Mayer and S. Cerrito","year":"2001","journal-title":"Studia Logica"},{"key":"10.2168\/LMCS-7(2:6)2011_CialdeaMayerCerrito10","unstructured":"M. Cialdea Mayer and S. Cerrito. Nominal substitution at work with the global and converse modalities. In L. Beklemishev, V. Goranko, and V. Shehtman, eds,Advances in Modal Logic, vol. 8, pp. 57-74. College Publications, 2010."},{"issue":"3","key":"10.2168\/LMCS-7(2:6)2011_DAgostinoMondadori-TC+-1994","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1093\/logcom\/4.3.285","volume":"4","author":"M. D'Agostino and M. Mondadori","year":"1994","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"10.2168\/LMCS-7(2:6)2011_FarinasDelCerroGasquet02","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1093\/jigpal\/10.1.51","volume":"10","author":"L. Fari\u00f1as del Cerro and O. Gasquet","year":"2002","journal-title":"Logic Journal of the IGPL"},{"key":"10.2168\/LMCS-7(2:6)2011_Fitting-PMMIL-1983","doi-asserted-by":"crossref","unstructured":"M. Fitting.Proof methods for modal and intuitionistic logics. Kluwer, 1983.","DOI":"10.1007\/978-94-017-2794-5"},{"key":"10.2168\/LMCS-7(2:6)2011_GasquetEtAl05","doi-asserted-by":"publisher","DOI":"10.1007\/11554554_25"},{"key":"10.2168\/LMCS-7(2:6)2011_GorankoShkatov09","unstructured":"V. Goranko and D. Shkatov. Tableau-based decision procedure for full coalitional multiagent temporal-epistemic logic of linear time. In C. Sierra, C. Castelfranchi, K. S. Decker, and J. S. Sichman, eds,Proceedings of the 8th International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS'09), pp. 969-976. IFAAMAS, 2009."},{"key":"10.2168\/LMCS-7(2:6)2011_Gore-TMMTL-1999","doi-asserted-by":"crossref","unstructured":"R. Gor\u00e9. Tableau methods for modal and temporal logics. In M. D'Agostino, D. M. Gabbay, R. H\u00e4hnle, and J. Posegga, eds,Handbook of Tableau Methods. Springer, 1999.","DOI":"10.1007\/978-94-017-1754-0_6"},{"key":"10.2168\/LMCS-7(2:6)2011_Heuerding98","unstructured":"A. Heuerding.Sequent calculi for proof search in some modal logics. PhD thesis, Universit\u00e4t Bern, 1998."},{"key":"10.2168\/LMCS-7(2:6)2011_HorrocksHustadtSattlerSchmidt07","doi-asserted-by":"crossref","unstructured":"I. Horrocks, U. Hustadt, U. Sattler, and R. A. Schmidt. Computational modal logic. In P. Blackburn, J. van Benthem, and F. Wolter, eds,Handbook of Modal Logic, pp. 181-245. Elsevier, 2007.","DOI":"10.1016\/S1570-2464(07)80007-3"},{"issue":"3","key":"10.2168\/LMCS-7(2:6)2011_HorrocksSattler-TDP_SHOIQ-2007","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/s10817-007-9079-9","volume":"39","author":"I. Horrocks and U. Sattler","year":"2007","journal-title":"Journal of Automated Reasoning"},{"key":"10.2168\/LMCS-7(2:6)2011_HughesCresswell68","unstructured":"G. E. Hughes and M. J. Cresswell.An Introduction to Modal Logic. Routledge, London, 1968."},{"key":"10.2168\/LMCS-7(2:6)2011_HustadtSchmidt99b","unstructured":"U. Hustadt and R. A. Schmidt. On the relation of resolution and tableaux proof systems for description logics. In T. Dean, ed.,Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI'99), pp. 110-115. Morgan Kaufmann, 1999."},{"key":"10.2168\/LMCS-7(2:6)2011_HustadtTishkovskyWolterZakharyaschev-ARMT-2006","unstructured":"U. Hustadt, D. Tishkovsky, F. Wolter, and M. Zakharyaschev. Automated reasoning about metric and topology (System description). In M. Fisher, W. van der Hoek, B. Konev, and A. Lisitsa, eds,Proceedings of the 10th European Conference on Logics in Artificial Intelligence (JELIA'06), vol. 4160 ofLecture Notes in Artificial Intelligence, pp. 490-493. Springer, 2006."},{"key":"10.2168\/LMCS-7(2:6)2011_Kripke-SAIL1-1965","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71685-9"},{"issue":"3","key":"10.2168\/LMCS-7(2:6)2011_Massacci00a","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1023\/A:1006155811656","volume":"24","author":"F. Massacci","year":"2000","journal-title":"Journal of Automated Reasoning"},{"key":"10.2168\/LMCS-7(2:6)2011_MotikShearerHorrocks09","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1613\/jair.2811","volume":"36","author":"B. Motik, R. Shearer, and I. Horrocks","year":"2009","journal-title":"Journal of Artificial Intelligence Research"},{"key":"10.2168\/LMCS-7(2:6)2011_Schmidt06b","unstructured":"R. A. Schmidt. Developing modal tableaux and resolution methods via first-order resolution. In G. Governatori, I. M. Hodkinson, and Y. Venema, eds,Advances in Modal Logic, Volume 6, pp. 1-26. College Publications, 2006."},{"key":"10.2168\/LMCS-7(2:6)2011_SchmidtTishkovsky-UTD+-2007","unstructured":"R. A. Schmidt and D. Tishkovsky. Using tableau to decide expressive description logics with role negation. In K. Aberer, K.-S. Choi, N. Noy, D. Allemang, K.-I. Lee, L. Nixon, J. Golbeck, P. Mika, D. Maynard, R. Mizoguchi, G. Schreiber, and P. Cudr\u00e9-Mauroux, eds,Proceedings of the 6th International Semantic Web Conference and the 2nd Asian Semantic Web Conference (ISWC'07), vol. 4825 ofLecture Notes in Computer Science, pp. 438-451. Springer, 2007."},{"key":"10.2168\/LMCS-7(2:6)2011_SchmidtTishkovsky-GTM+-2008","unstructured":"R. A. Schmidt and D. Tishkovsky. A general tableau method for deciding description logics, modal logics and related first-order fragments. In A. Armando, P. Baumgartner, and G. Dowek, eds,Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR'08), vol. 5195 ofLecture Notes in Computer Science, pp. 194-209. Springer, 2008."},{"key":"10.2168\/LMCS-7(2:6)2011_SchmidtTishkovsky-ASTC-2009","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02716-1_23"},{"key":"10.2168\/LMCS-7(2:6)2011_mettel_page","unstructured":"D. Tishkovsky. MetTeL system. http:\/\/www.mettel-prover.org."},{"key":"10.2168\/LMCS-7(2:6)2011_TishkovskySchmidtKhodadadi11","doi-asserted-by":"crossref","unstructured":"D. Tishkovsky, R. A. Schmidt, and M. Khodadadi. MetTeL: A tableau prover with logic-independent inference engine. In G. Metcalfe and K. Br\u00fcnnler, eds,Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'11), Lecture Notes in Computer Science. Springer, 2011. To appear.","DOI":"10.1007\/978-3-642-22119-4_19"},{"key":"10.2168\/LMCS-7(2:6)2011_Tzakova99","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48754-9_24"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/970\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/970\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:00:14Z","timestamp":1681243214000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/970"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5,7]]},"references-count":37,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(2:6)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1104.4131","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1104.4131","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"arxiv","id":"1611.09014","asserted-by":"subject"},{"id-type":"doi","id":"10.1007\/s10817-019-09515-1","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arxiv.1611.09014","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2011,5,7]]},"article-number":"970"}}