Abstract
In this paper, written to honor the career of Ewa Orłowska, we survey the main results on dual tableau-based decision procedures for fragments of the logic of binary relations. Specifically, we shall review relational fragments representing well known classes of first-order logic, of modal and multi-modal logics, and of description logics. We shall also examine a relational fragment admitting the use of a simple form of entailment within dual tableau decision procedures.
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
Notes
- 1.
With a slight abuse of notation, the Boolean operators ‘\(\cap \)’, ‘\(\cup \)’ will also be used as n-ary operators, for \(n \ge 2\), by exploiting their associativity.
- 2.
We recall that \(\forall \forall (\exists )\) denotes the class of prenex formulae with exactly two universal quantifiers followed by any number of existential quantifiers.
- 3.
Table 7.7 does not contain any decomposition rule for the converse operator ‘\({}^{{\mathop {{-}}}1}\)’ because it is not a constructor of the terms belonging to the \((\mathsf {r}\mathbin {{\varvec{;}}}\_)\)-fragment.
- 4.
Metavariables \(x,y,z,x',\ldots \), used from now on in place of individual variables, stand for arbitrary but fixed individual variables.
- 5.
From now on, we identify nodes with the (disjunctive) sets labelling them.
- 6.
Notice that the \((\{{\mathbf {1}},\cup ,\cap \}\mathbin {{\varvec{;}}}\_)\)-fragment does not admit the operator ‘\((\cdot )^{\mathop {\mathop {{-}}1}}\)’.
References
Baader, F., Calvanese, D., McGuinness, D. L., Nardi, D., & Patel-Schneider, P. F. (Eds.). (2003). The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge: Cambridge University Press.
Baader, F. (2009). Description logics. In S. Tessaris et al. (Eds.), Reasoning Web. Semantic Technologies for Information Systems, 5th International Summer School 2009, Tutorial Lectures (Vol. 5689, pp. 1–39). Lecture Notes in Computer Science. Brixen-Bressanone: Springer.
Beth, W. E. (1955). Semantic entailment and formal derivability. Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde,18(13), 309–342 (reprinted in Hintikka, 1969).
Cantone, D., Nicolosi Asmundo, M., & Orłowska, E. (2010). Dual tableau-based decision procedures for some relational logics. In W. Faber & N. Leone (Eds.), Proceedings of the 25th Italian Conference on Computational Logic (Vol. 598). CEUR Workshop Proceedings. Rende, Italy. http://CEUR-WS.org.
Cantone, D., Nicolosi Asmundo, M., & Orłowska, E. (2011). Dual tableau-based decision procedures for relational logics with restricted composition operator. Journal of Applied Non-classical Logics, 21(2), 177–200.
Cantone, D., Golińska-Pilarek, J., & Asmundo, M. N. (2014a). A relational dual tableau decision procedure for multimodal and description logics. In M. M. Polycarpou et al. (Eds.), 9th International Conference Proceedings of Hybrid Artificial Intelligence Systems HAIS 2014 (Vol. 8480, pp. 466–477). Lecture Notes in Computer Science. Salamanca: Springer.
Cantone, D., Nicolosi Asmundo, M., & Orłowska, E. (2014b). In L. Giordano, V. Gliozzi, & G. Pozzato (Eds.), Proceedings of the 29th Italian Conference on Computational Logic (Vol. 1195, pp. 194–209). CEUR Workshop Proceedings. Torino, Italy. http://CEUR-WS.org.
Cantone, D., Nicolosi Asmundo, M., & Orłowska, E. (2018). A dual tableau-based decision procedure for a relational logic with the universal relation (extended version). CoRR. arXiv:1802.07508.
Dershowitz, N. & Jouannaud, J.-P. (1990). Rewrite systems. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) (pp. 243–320).
Fitting, M. (1996). First-order Logic and Automated Theorem Proving (2nd ed.). Graduate Texts in Computer Science. Berlin: Springer.
Formisano, A. & Nicolosi Asmundo, M. (2006). An efficient relational deductive system for propositional non-classical logics. Journal of Applied Non-classical Logics, 16(3–4), 367–408.
Glivenko, V. (1929). Sur quelques points de la logique de m. brouwer. Bulletins de la Classe des Sciences,5(15), 183–188.
Golińska-Pilarek, J. & Orłowska, E. (2007). Tableaux and dual tableaux: Transformation of proofs. Studia Logica, 85(3), 291–310.
Golińska-Pilarek, J., Muñoz-Velasco, E., & Mora, A. (2011). A new deduction system for deciding validity in modal logic K. Logic Journal of the IGPL, 19(2), 425–434.
Golińska-Pilarek, J., Muñoz-Velasco, E., & Mora Bonilla, A. (2012). Relational dual tableau decision procedure for modal logic K. Logic Journal of the IGPL, 20(4), 747–756.
Golińska-Pilarek, J., Huuskonen, T., & Muñoz-Velasco, E. (2014). Relational dual tableau decision procedures and their applications to modal and intuitionistic logics. Annals of Pure and Applied Logic, 165(2), 409–427.
Konikowska, B. (2002). Rasiowa-Sikorski deduction systems in computer science applications. Theoretical Computer Science, 286(2), 323–366.
Mints, G. (1988). Gentzen-type systems and resolution rules. Part I. Propositional logic. In P. Martin-Löf & G. Mints (Eds.), Proceedings of COLOG-88, International Conference on Computer Logic (Vol. 417, pp. 198–231). Lecture Notes in Computer Science. Tallinn: Springer.
Mora, A., Muñoz-Velasco, E., & Golińska-Pilarek, J. (2011). Implementing a relational theorem prover for modal logic. International Journal of Computer Mathematics, 88(9), 1869–1884.
Orłowska, E. (1988). Relational interpretation of modal logics. In H. Andreka, D. Monk, & I. Németi (Eds.), Algebraic Logic. Colloquia Mathematica Societatis Janos Bolyai (Vol. 54, pp. 443–471). Amsterdam: North Holland.
Orłowska, E. & Golińska-Pilarek, J. (2011). Dual Tableaux: Foundations, Methodology, Case Studies. Trends in Logic. Dordrecht-Heidelberg-London-New York: Springer.
Rasiowa, H. & Sikorski, R. (1960). On the Gentzen theorem. Fundamenta Mathematicae, 48, 57–69.
Rasiowa, H. & Sikorski, R. (1963). The Mathematics of Metamathematics. Warszawa: Polish Scientific Publishers.
Sattler, U. (1996). A concept language extended with different kinds of transitive roles. In G. Görz & S. Hölldobler (Eds.), 20th Annual German Conference on Artificial Intelligence Proceedings of KI-96: Advances in Artificial Intelligence (Vol. 1137, pp. 333–345). Lecture Notes in Computer Science. Dresden: Springer.
Tarski, A. & Givant, S., (1987). Formalization of Set Theory Without Variables. Colloquium Publications. Providence: American Mathematical Society.
Acknowledgements
The authors would like to thank the anonymous reviewers for their very helpful comments. This work was supported by the Polish National Science Centre research project DEC-2011/02/A/HS1/00395.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Cantone, D., Nicolosi-Asmundo, M. (2018). Dual Tableau-Based Decision Procedures for Fragments of the Logic of Binary Relations. In: Golińska-Pilarek, J., Zawidzki, M. (eds) Ewa Orłowska on Relational Methods in Logic and Computer Science. Outstanding Contributions to Logic, vol 17. Springer, Cham. https://doi.org/10.1007/978-3-319-97879-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-97879-6_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-97878-9
Online ISBN: 978-3-319-97879-6
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)