Abstract
This article presents labelled sequent calculi \(\mathcal{{S}_{ALC}}\) and \(\mathcal{{S}^{[]}_{ALC}}\) for the basic Description Logic (DL) \(\mathcal{ALC}\). Proposing Sequent Calculus (SC) for dealing with DL reasoning aims to provide a more structural way to generated explanations, from proofs as well as counter-models, in the context of Knowledge Base and Ontologies authoring tools. The ability of providing short (Polynomial) proofs is also considered as an advantage of SC-based explanations with regard to the well-known Tableaux-based reasoners. Both, \(\mathcal{{S}_{ALC}}\) and \(\mathcal{{S}^{[]}_{ALC}}\) satisfy cut-elimination, while \(\mathcal{{S}^{[]}_{ALC}}\) also provides \(\mathcal{ALC}\) counter-example from unsuccessful proof-trees. Some suggestions for extracting explanations from proofs in the presented systems is also discussed.
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 subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Schmidt-Schau, M., Smolka, G.: Attributive concept descriptions with complements. Artificial Intelligence 48(1), 1–26 (1991)
McGuinness, D.: Explaining Reasoning in Description Logics. PhD thesis, Rutgers University (1996)
Liebig, T., Halfmann, M.: Explaining subsumption in \(\mathcal{ALEHF}_{R^+}\) tboxes. In: Horrocks, I., Sattler, U., Wolter, F. (eds.) Proc. of the 2005 International Workshop on Description Logics - DL 2005, Edinburgh, Scotland, pp. 144–151 (July 2005)
Deng, X., Haarslev, V., Shiri, N.: Using patterns to explain inferences in \(\mathcal{ALCHI}\). Computational Intelligence 23(3), 386–406 (2007)
Gordeev, L., Haeusler, E., Costa, V.: Proof compressions with circuit-structured substitutions. In: Zapiski Nauchnyh Seminarov POMI (to appear, 2008)
Finger, M., Gabbay, D.: Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs. Logic Journal of the IGPL 15(5–6), 553–575 (2007)
Baader, F.: The Description Logic Handbook: theory, implementation, and applications. Cambridge University Press, Cambridge (2003)
Rademaker, A., do Amaral, F., Haeusler, E.: A Sequent Calculus for \(\mathcal{ALC}\). Monografias em Ciência da Computação 25/07, Departamento de Informática, PUC-Rio (2007)
Rademaker, A., Haeusler, E., Pereira, L.: On the proof theory of \(\mathcal{ALC}\). In: XV EBL -15th Brazilian Logic Conference (to appear)
Finger, M.: DAG sequent proofs with a substitution rule. In: Artemov, S., Barringer, H., dAvila Garcez, A., Lamb, L., Woods, J. (eds.) We will show Them – Essays in honour of Dov Gabbays 60th birthday, vol. 1, pp. 671–686. Kings College Publications, London (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rademaker, A., Haeusler, E.H. (2008). Toward Short and Structural \(\mathcal{ALC}\)-Reasoning Explanations: A Sequent Calculus Approach. In: Zaverucha, G., da Costa, A.L. (eds) Advances in Artificial Intelligence - SBIA 2008. SBIA 2008. Lecture Notes in Computer Science(), vol 5249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88190-2_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-88190-2_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88189-6
Online ISBN: 978-3-540-88190-2
eBook Packages: Computer ScienceComputer Science (R0)