Abstract
This paper presents a method for synthesising sound and complete tableau calculi. Given a specification of the formal semantics of a logic, the method generates a set of tableau inference rules which can then be used to reason within the logic. The method guarantees that the generated rules form a calculus which is sound and constructively complete. If the logic can be shown to admit finite filtration with respect to a well-defined first-order semantics then adding a general blocking mechanism produces a terminating tableau calculus. The process of generating tableau rules can be completely automated and produces, together with the blocking mechanism, an automated procedure for generating tableau decision procedures. For illustration we show the workability of the approach for propositional intuitionistic logic.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Horrocks, I., Sattler, U.: A tableau decision procedure for SHOIQ. J. Automat. Reasoning 39(3), 249–276 (2007)
Hustadt, U., Tishkovsky, D., Wolter, F., Zakharyaschev, M.: Automated reasoning about metric and topology (System description). In: Fisher, M., van der Hoek, W., Konev, B., Lisitsa, A. (eds.) JELIA 2006. LNCS(LNAI), vol. 4160, pp. 490–493. Springer, Heidelberg (2006)
Kripke, S.A.: Semantical analysis of intuitionistic logic I. In: Formal Systems and Recursive Functions, pp. 92–130. North-Holland, Amsterdam (1965)
Schmidt, R.A.: Developing modal tableaux and resolution methods via first-order resolution. In: Advances in Modal Logic, vol. 6, pp. 1–26. College Publ. (2006)
Schmidt, R.A., Tishkovsky, D.: Using tableau to decide expressive description logics with role negation. In: Aberer, K., Choi, K.-S., Noy, N., Allemang, D., Lee, K.-I., Nixon, L., Golbeck, J., Mika, P., Maynard, D., Mizoguchi, R., Schreiber, G., Cudré-Mauroux, P. (eds.) ASWC 2007 and ISWC 2007. LNCS, vol. 4825, pp. 438–451. Springer, Heidelberg (2007)
Schmidt, R.A., Tishkovsky, D.: A general tableau method for deciding description logics, modal logics and related first-order fragments. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 194–209. Springer, Heidelberg (2008)
Schmidt, R.A., Tishkovsky, D.: Automated synthesis of tableau calculi (2009), http://www.cs.man.ac.uk/~dmitry/papers/astc2009.pdf
Tishkovsky, D.: MetTeL system, http://www.cs.man.ac.uk/~dmitry/implementations/MetTeL/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schmidt, R.A., Tishkovsky, D. (2009). Automated Synthesis of Tableau Calculi. In: Giese, M., Waaler, A. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2009. Lecture Notes in Computer Science(), vol 5607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02716-1_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-02716-1_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02715-4
Online ISBN: 978-3-642-02716-1
eBook Packages: Computer ScienceComputer Science (R0)