This article presents labelled sequent calculi and for the basic Description Logic (DL) . 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, and satisfy cut-elimination, while also provides counter-example from unsuccessful proof-trees. Some suggestions for extracting explanations from proofs in the presented systems is also discussed. © 2008 Springer Berlin Heidelberg.
CITATION STYLE
Rademaker, A., & Haeusler, E. H. (2008). Toward short and structural ALC-reasoning explanations: A sequent calculus approach. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5249 LNAI, pp. 167–176). Springer Verlag. https://doi.org/10.1007/978-3-540-88190-2_22
Mendeley helps you to discover research relevant for your work.