Abstract
Description Logics have well-known and mature proof procedures based on Tableaux for reasoning on Ontologies and Knowledge Bases. The task of understanding the outcomes of formal proof procedure or consistency tests is sometimes quite hard. Explanations on the reasons for some subsumptions either hold or not are demanding. The latter is in general supported by a human-readable translation of the witness construction obtained by the usual, first-order inspired, Tableaux DL procedure. For the former, however, an explanation should be obtained from the proof resulted by this very Tableaux procedure. In this chapter, we review our contributions and present some possible future works.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Baader, F.: The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003)
Baader, F., Peñaloza, R., Suntisrivaraporn, B.: Pinpointing in the description logic \({\rm {el}}+{\cal {EL}}^{+}\). In: Proceedings of the 30th annual German Conference on Advances in Artificial Intelligence, Osnabrück, Germany KI ’07, Lecture Notes in Computer Science. vol. 4667/2007, pp. 52–67. Springer-Verlag, Berlin, Heidelberg (2007). ISBN:978-3-540-74564-8, doi:10.1007/978-3-540-74565-5_7
Bail, S., Horridge, M., Parsia, B., Sattler, U.: The justificatory structure of the ncbo bioportal ontologies. The Semantic Web-ISWC 2011, pp. 67–82 (2011)
Bozzato, L., Ferrari, M., Fiorentini, C., Fiorino, G.: A constructive semantics for ALC. In: Workshop on Description Logics, pp. 219–226. (2007)
Finger, M.: DAG sequent proofs with a substitution rule. In: Artemov, S., Barringer, H., d’Avila Garcez, A., Lamb, L., Woods, J. (eds.) We will show Them–Essays in honour of Dov Gabbay 60th birthday, vol. 1, pp. 671–686. Kings College Publications, Kings College, London (2005)
Gabbay, D.M.: Labelled deductive systems, vol. 1. Oxford University Press, Oxford (1996)
Gordeev, L., Haeusler, E., Costa, V.: Proof compressions with circuit-structured substitutions. In: Zapiski Nauchnyh Seminarov POMI, (2008) to appear
Haeusler, E.H., de Paiva, V., Rademaker, A.: Intuitionistic description logic and legal reasoning. In: Proceedings of International Workshop Data, Logic and Inconsistency with DEXA, (2011). (2011)
Haeusler, E.H., de Paiva, V., Rademaker, A.: Using intuitionistic logic as a basis for legal ontologies. Informatica e Diritto (Journal on Informatics and Law), 1–2:289–298, (2010)
Horridge, M., Parsia, B., Sattler, U.: Laconic and precise justifications in owl. The Semantic Web-ISWC 2008 pp. 323–338. (2008)
Ji, Q., Qi, G., Haase, P.: A relevance-directed algorithm for finding justifications of dl entailments. The Semantic Web pp. 306–320. (2009)
Kalyanpur, A., Parsia, B., Horridge, M., Sirin, E.: Finding all justifications of owl dl entailments. The Semantic Web pp. 267–280. (2007)
Mendler, M., Scheele, S.: Towards constructive DL for abstraction and refinement. In: F. Baader, C. Lutz, B. Motik (eds.) Proceedings of the 21st International Workshop on Description Logics, CEUR Workshop Proceedings, vol. 353, pp. 13–16. CEUR-WS.org, Dresden, Germany (2008). http://www.ceur-ws.org/Vol-353/MendlerScheele.pdf
de Paiva, V.: Constructive description logics: what, why and how. In: Context Representation and Reasoning. Riva del Garda (2006)
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2012 The Author(s)
About this chapter
Cite this chapter
Rademaker, A. (2012). Conclusion. In: A Proof Theory for Description Logics. SpringerBriefs in Computer Science. Springer, London. https://doi.org/10.1007/978-1-4471-4002-3_9
Download citation
DOI: https://doi.org/10.1007/978-1-4471-4002-3_9
Published:
Publisher Name: Springer, London
Print ISBN: 978-1-4471-4001-6
Online ISBN: 978-1-4471-4002-3
eBook Packages: Computer ScienceComputer Science (R0)