Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Reasoning with Analytic Tableaux and Related Methods

TABLEAUX 2009: Automated Reasoning with Analytic Tableaux and Related Methods pp 205–219Cite as

Sound Global State Caching for ALC with Inverse Roles

  • Conference paper

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

Abstract

We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability with respect to a TBox in the logic ALCI using global state caching. Global state caching guarantees optimality and termination without dynamic blocking, but in the presence of inverse roles, the proofs of soundness and completeness become significantly harder. We have implemented the algorithm in OCaml, and our initial comparison with FaCT++ indicates that it is a promising method for checking satisfiability with respect to a TBox.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P. (eds.): The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  3. Horrocks, I., Patel-Schneider, P.F.: Optimizing description logic subsumption. Journal of Logic and Computation 9(3), 267–293 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  4. Donini, F.M., Massacci, F.: EXPTIME tableaux for ALC. Artificial Intelligence 124(1), 87–138 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  5. Goré, R., Nguyen, L.A.: EXPTIME tableaux for ALC using sound global caching. In: Proc. DL 2007. CEUR Workshop, vol. 250 (2007), CEUR-WS.org

  6. Goré, R., Postniece, L.: An experimental evaluation of global caching for ALC (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 299–305. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  7. Goré, R., Nguyen, L.A.: EXPTIME tableaux with global caching for description logics with transitive roles, inverse roles and role hierarchies. In: Olivetti, N. (ed.) TABLEAUX 2007. LNCS, vol. 4548, pp. 133–148. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  8. Blackburn, P., Wolter, F., van Benthem, J. (eds.): Handbook of Modal Logic. Elsevier, Amsterdam (2006)

    Google Scholar 

  9. Ding, Y., Haarslev, V., Wu, J.: A new mapping from ALCI to ALC. In: Proc. DL-2007. CEUR Workshop Proceedings, vol. 250 (2007), CEUR-WS.org

Download references

Author information

Authors and Affiliations

  1. Logic and Computation Group, The Australian National University, Canberra, ACT 0200, Australia

    Rajeev Goré

  2. Logic and Computation Group and NICTA, The Australian National University, Canberra, ACT 0200, Australia

    Florian Widmann

Authors
  1. Rajeev Goré
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Florian Widmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Informatics, University of Oslo, Blindern, P.O. Box 1080, 0316, Oslo, Norway

    Martin Giese  & Arild Waaler  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Goré, R., Widmann, F. (2009). Sound Global State Caching for ALC with Inverse Roles. 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_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02716-1_16

  • 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)

Publish with us

Policies and ethics

Search

Navigation