Skip to main content
SpringerLink
Log in

A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies

  • Conference paper
Book cover Automated Deduction – CADE-24 (CADE 2013)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 7898))

Included in the following conference series:

Abstract

A tableau calculus constituting a decision procedure for hybrid logic with the converse modalities, the global ones and a restricted use of the binder has been defined in a previous paper. This work shows how to extend such a calculus to multi-modal logic equipped with two features largely used in description logics, i.e. transitivity and relation inclusion assertions. An implementation of the proof procedure is also briefly presented, along with the results of some preliminary experiments.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Areces, C., Blackburn, P., Marx, M.: A road-map on complexity for hybrid logics. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 307–321. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  2. Areces, C., Heguiabehere, J.: hGen: A random CNF formula generator for hybrid languages. In: Methods for Modalities 3 (M4M-3), Nancy, France (2003)

    Google Scholar 

  3. Areces, C., ten Cate, B.: Hybrid logics. In: Handbook of Modal Logics, pp. 821–868. Elsevier (2007)

    Google Scholar 

  4. Blackburn, P., Seligman, J.: Hybrid languages. Journal of Logic, Language and Information 4, 251–272 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bolander, T., Blackburn, P.: Terminating tableau calculi for hybrid logics extending K. Electronic Notes in Theoretical Computer Science 231, 21–39 (2009)

    Article  MathSciNet  Google Scholar 

  6. Cerrito, S., Cialdea Mayer, M.: An efficient approach to nominal equalities in hybrid logic tableaux. Journal of Applied Non-classical Logics 20(1-2), 39–61 (2010)

    Google Scholar 

  7. Cerrito, S., Cialdea Mayer, M.: Nominal substitution at work with the global and converse modalities. In: Advances in Modal Logic, vol. 8, pp. 57–74. College Publications (2010)

    Google Scholar 

  8. Cerrito, S., Cialdea Mayer, M.: A tableaux based decision procedure for a broad class of hybrid formulae with binders. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 104–118. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  9. Cerrito, S., Cialdea Mayer, M.: A tableau based decision procedure for a fragment of hybrid logic with binders. Journal of Automated Reasoning (2012) (published online, to appear on paper)

    Google Scholar 

  10. Cialdea Mayer, M.: Tableaux for multi-modal hybrid logic with binders, transitive relations and relation hierarchies. Technical Report RT-DIA-199-2012, Dipartimento di Informatica e Automazione, Università di Roma Tre (2012)

    Google Scholar 

  11. Cialdea Mayer, M., Cerrito, S.: Herod and Pilate: two tableau provers for basic hybrid logic. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 255–262. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  12. Grädel, E.: On the restraining power of guards. Journal of Symbolic Logic 64, 1719–1742 (1998)

    Article  Google Scholar 

  13. Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. Journal of Logic and Computation 9(3), 385–410 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  14. Horrocks, I., Sattler, U.: A tableau decision procedure for \(\mathcal{SHOIQ}\). Journal of Automated Reasoning 39(3), 249–276 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  15. Kaminski, M., Schneider, S., Smolka, G.: Terminating tableaux for graded hybrid logic with global modalities and role hierarchies. Logical Methods in Computer Science 7(1) (2011)

    Google Scholar 

  16. Kaminski, M., Smolka, G.: Terminating tableau systems for hybrid logic with difference and converse. Journal of Logic, Language and Information 18(4), 437–464 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  17. Mundhenk, M., Schneider, T.: Undecidability of multi-modal hybrid logics. Electronic Notes in Theoretical Computer Science 174(6), 29–43 (2007)

    Article  Google Scholar 

  18. Mundhenk, M., Schneider, T., Schwentick, T., Weber, V.: Complexity of hybrid logics over transitive frames. Journal of Applied Logic 8(4), 422–440 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  19. Szwast, W., Tendera, L.: On the decision problem for the guarded fragment with transitivity. In: Proc. of the 16th Symposium on Logic in Computer Science (LICS), pp. 147–156 (2001)

    Google Scholar 

  20. ten Cate, B., Franceschet, M.: On the complexity of hybrid logics with binders. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 339–354. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  21. Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Università di Roma Tre, Italy

    Marta Cialdea Mayer

Authors
  1. Marta Cialdea Mayer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università degli Studi di Verona, Strada Le Grazie 15, 37134, Verona, Italy

    Maria Paola Bonacina

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cialdea Mayer, M. (2013). A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies. In: Bonacina, M.P. (eds) Automated Deduction – CADE-24. CADE 2013. Lecture Notes in Computer Science(), vol 7898. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38574-2_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-38574-2_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-38573-5

  • Online ISBN: 978-3-642-38574-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation