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

摘要

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 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.