Providing a Proof-Theoretical Basis for Explanation: A Case Study on UML and ALCQI Reasoning

Alexandre Rademaker (PUC-Rio, Brazil)

Edward Hermann Haeusler (PUC-Rio, Brazil)

Abstract: In this article we argue in favour of Natural Deduction Systems as a basis for formal proof explanations. We illustrate our choice presenting a Natural Deduction for ALCQI and use it to help explain UML reasoning.

Keywords: ALC, ALCQI, Description Logics, Proof Theory, Sequent Calculus, UML, natural deduction

Categories: F.4.1, M.4