Skip to main content
SpringerLink
Log in

A Connection Calculus for the Description Logic \( {\mathcal{ALC}} \)

  • Conference paper
  • First Online:
Advances in Artificial Intelligence (Canadian AI 2016)

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

Included in the following conference series:

Abstract

This paper presents a connection calculus for the description logic (DL) \( {\mathcal{ALC}} \). It replaces the usage of Skolem terms and unification by additional annotation and introduces blocking, a typical feature of DL provers, by a new rule, to ensure termination in the case of cyclic ontologies. Besides the connection calculus, a simplified clausal form normalization is presented. Furthermore, termination, soundness and completeness of the calculus are proven.

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 EPUB and 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

Notes

  1. 1.

    The symbols E and Ê were chosen here to designate a concept name and a pure conjunction rather than the usual C and Ĉ, to avoid confusion with clauses, that are also denoted by C.

  2. 2.

    If \(\exists r.\top \) ⊑ \( \hat{E} \) or \( \forall r. \) ⊑ \( \check{D} \in \bot {\mathcal{T}} \), then the matrix must include axioms \( A \) ⊑ \( \top \), for all A ∈ N C , too. Conversely, \(\exists r.\top \) ⊑ \( \hat{E} \) or \(\forall r. \top \) ⊑ \( \check{D}\) requires axioms \( \bot \) ⊑ \( A \), for all A ∈ N C , in the matrix.

References

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

    MATH  Google Scholar 

  2. Bibel, W.: Automated Theorem Proving. Vieweg Verlag, Wiesbaden (1987)

    Book  MATH  Google Scholar 

  3. Freitas, F.: A connection method for inferencing over the description logic ALC. In: Description Logics Workshop, Barcelona, Spain (2011)

    Google Scholar 

  4. Melo, D., Otten, J., Freitas, F.: RACCOON: an experimental automated reasoner for description logics using a modified version of the connection method (2016). https://github.com/dmfilho/raccoon

  5. Ghilardi, S., Lutz, C., Wolter, F.: Did I damage my ontology: a case of conservative extensions of description logics. In: Proceedings of 10th International Conference of Principles of KR&R (KR). AAAI Press (2006)

    Google Scholar 

  6. Graedel, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: Proceedings of 12th IEEE Symposium on Logic in Computer Science, LICS 1997 (1997)

    Google Scholar 

  7. Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. J. Logic Comput. 9(3), 385–410 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  8. Mortimer, M.: On languages with two variables. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 21, 135–140 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  9. Otten, J.: Restricting backtracking in connection calculi. AI Commun. 23(2–3), 159–182 (2010)

    MathSciNet  MATH  Google Scholar 

  10. Schlicht, A., Stuckenschmidt, H.: Peer-to-peer reasoning for interlinked ontologies. Int. J. Seman. Comput. 4(1), 27–58 (2010). (Special Issue on Web Scale Reasoning)

    Article  MATH  Google Scholar 

  11. Schmidt, R., Tishkovsky, D.: Analysis of blocking mechanisms for description logics. In: Proceedings of the Workshop on Automated Reasoning (2007)

    Google Scholar 

  12. Tsarkov, D., Riazanov, A., Bechhofer, S., Horrocks, I.: Using vampire to reason with OWL. In: McIlraith, S.A., Plexousakis, D., van Harmelen, F. (eds.) ISWC 2004. LNCS, vol. 3298, pp. 471–485. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

Download references

Acknowledgements

The authors would like to thank Pernambuco’s state sponsoring agency FACEPE for a grant to support the stay of Jens Otten at UFPE.

Author information

Authors and Affiliations

  1. Informatics Center, Federal University of Pernambuco (CIn - UFPE), Recife, Brazil

    Fred Freitas & Jens Otten

  2. Institut für Informatik, University of Potsdam, Potsdam, Germany

    Jens Otten

Authors
  1. Fred Freitas
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jens Otten
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Fred Freitas .

Editor information

Editors and Affiliations

  1. Lakehead University, Thunder Bay, Ontario, Canada

    Richard Khoury

  2. National Research Council Canada , Ottawa, Canada

    Christopher Drummond

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Freitas, F., Otten, J. (2016). A Connection Calculus for the Description Logic \( {\mathcal{ALC}} \) . In: Khoury, R., Drummond, C. (eds) Advances in Artificial Intelligence. Canadian AI 2016. Lecture Notes in Computer Science(), vol 9673. Springer, Cham. https://doi.org/10.1007/978-3-319-34111-8_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-34111-8_30

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-34110-1

  • Online ISBN: 978-3-319-34111-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation