Abstract
Our interest in this paper are semantic tableau approaches closely related to bottom-up model generation methods. Using equality-based blocking techniques these can be used to decide logics representable in first-order logic that have the finite model property. Many common modal and description logics have these properties and can therefore be decided in this way. This paper integrates congruence closure, which is probably the most powerful and efficient way to realise reasoning with ground equations, into a modal tableau system with equality-based blocking. The system is described for an extension of modal logic K characterised by frames in which the accessibility relation is transitive and every world has a distinct immediate predecessor. We show the system is sound and complete, and discuss how various forms of blocking such as ancestor blocking can be realised in this setting. Though the investigation is focussed on a particular modal logic, the modal logic was chosen to show the most salient ideas and techniques for the results to be generalised to other tableau calculi and other logics.
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.
Similar content being viewed by others
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)
Baader, F., Sattler, U.: An overview of tableau algorithms for description logics. Studia Logica 69, 5–40 (2001)
Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. Journal of Automated Reasoning 31(2), 129–168 (2003)
Baumgartner, P., Schmidt, R.A.: Blocking and other enhancements for bottom-up model generation methods. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 125–139. Springer, Heidelberg (2006)
Beckert, B.: Semantic tableaux with equality. Journal of Logic and Computation 7(1), 39–58 (1997)
Bolander, T., Blackburn, P.: Termination for hybrid tableaus. Journal of Logic and Computation 17(3), 517–554 (2007)
Bry, F., Manthey, R.: Proving finite satisfiability of deductive databases. In: Börger, E., Kleine Büning, H., Richter, M.M. (eds.) CSL 1987. LNCS, vol. 329, pp. 44–55. Springer, Heidelberg (1988)
Degtyarev, A., Voronkov, A.: Equality reasoning in sequent-based calculi. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 611–706. Elsevier (2001)
Giese, M.: Superposition-based equality handling for analytic tableaux. Journal of Automated Reasoning 38(1-3), 127–153 (2007)
Goré, R.: Tableau methods for modal and temporal logics. In: D’Agostino, M., Gabbay, D., Hähnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 297–396. Kluwer (1999)
Kaminski, M.: Incremental Decision Procedures for Modal Logics with Nominals and Eventualities. PhD thesis, Universität des Saarlandes, Germany (2012)
Kaminski, M., Smolka, G.: Hybrid tableaux for the difference modality. Electronic Notes in Theoretical Computer Science 231, 241–257 (2009)
Käufl, T., Zabel, N.: Cooperation of decision procedures in a tableau-based theorem prover. Revue d’Intelligence Artificielle 4(3), 99–126 (1990)
Khodadadi, M.: Exploration of Variations of Unrestricted Blocking for Description Logics. PhD thesis, The University of Manchester, UK (2015)
Khodadadi, M., Schmidt, R.A., Tishkovsky, D.: An abstract tableau calculus for the description logic \({\mathcal SHOI}\) using unrestricted blocking and rewriting. In: Proc. DL 2012. CEUR Workshop Proc., vol. 846. CEUR-WS.org (2012)
Khodadadi, M., Schmidt, R.A., Tishkovsky, D.: A refined tableau calculus with controlled blocking for the description logic \(\mathcal{SHOI}\). In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS, vol. 8123, pp. 188–202. Springer, Heidelberg (2013)
Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. Journal of the ACM 27(2), 356–364 (1980)
Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Information and Computation 205(4), 557–580 (2007)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53(6), 937–977 (2006)
Schmidt, R.A., Tishkovsky, D.: Using tableau to decide expressive description logics with role negation. In: Aberer, K., et al. (eds.) ASWC 2007 and ISWC 2007. LNCS, vol. 4825, pp. 438–451. Springer, Heidelberg (2007)
Schmidt, R.A., Tishkovsky, D.: Automated synthesis of tableau calculi. Logical Methods in Computer Science 7(2), 1–32 (2011)
Schmidt, R.A., Tishkovsky, D.: Using tableau to decide description logics with full role negation and identity. ACM Transactions on Computational Logic 15(1) (2014)
Schmidt, R.A., Waldmann, U.: Modal tableau systems with blocking and congruence closure. eScholar Report uk-ac-man-scw:268816, University of Manchester (2015)
Tishkovsky, D., Schmidt, R.A.: Refinement in the tableau synthesis framework (2013). arXiv e-Print 1305.3131v1 [cs.LO]
Tishkovsky, D., Schmidt, R.A., Khodadadi, M.: The tableau prover generator MetTeL2. In: del Cerro, L.F., Herzig, A., Mengin, J. (eds.) JELIA 2012. LNCS, vol. 7519, pp. 492–495. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Schmidt, R.A., Waldmann, U. (2015). Modal Tableau Systems with Blocking and Congruence Closure. In: De Nivelle, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2015. Lecture Notes in Computer Science(), vol 9323. Springer, Cham. https://doi.org/10.1007/978-3-319-24312-2_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-24312-2_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24311-5
Online ISBN: 978-3-319-24312-2
eBook Packages: Computer ScienceComputer Science (R0)