Toward Short and Structural ALC-Reasoning Explanations: A Sequent Calculus Approach

Abstract:

This article presents labelled sequent calculi S_ALC and S_ALC^[] for the basic Description Logic (DL) 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 \em SC-based explanations with regard to the well-known Tableaux-based reasoners. Both, S_ALC and S_ALC satisfy cut-elimination, while S_ALC^[] also provides ALC counter-example from unsuccessful proof-trees. Some suggestions for extracting explanations from proofs in the presented systems is also discussed. Keywords: description logics, sequent calculus, proof theory.

Downloads:

• full text
• No slides available

BibTeX:

@inproceedings{publication-25,
  author = {Rademaker, Alexandre and Haeusler, Edward Hermann},
  title = {Toward Short and Structural ALC-Reasoning Explanations: A Sequent Calculus Approach},
  booktitle = {Advances in Artificial Intelligence - SBIA 2008},
  year = {2008},
  publisher = {Springer Berlin},
  address = {Heidelberg},
  isbn = {9783540881896},
  pdflink1 = {/files/sbia2008.pdf},
  doi = {10.1007/978-3-540-88190-2_22},
  url = {http://dx.doi.org/10.1007/978-3-540-88190-2\_22}
}