Formal explanations as logical derivations

According to a longstanding philosophical tradition dating back to Aristotle, certain proofs do not only certify the truth of their conclu- sion but also explain it. Lately, much effort is being devoted to log- ically characterise the explanatory relation of grounding, especially by proof-theoretical means. Nevertheless, no thorough investigation of the resulting notion of formal explanation exists. We show that formal explanations can be seen as logical derivations of a particu- lar kind and study the interactions between grounding and logical rules, formal explanations and logical derivations. We define a min- imal calculus that captures both grounding and logical derivability, and show by a normalisation procedure that grounding rules are proof-theoretically balanced with respect to logical elimination rules. The introduced calculus enables us to combine logical derivations and explanations, to distinguish explanatory parts of derivations from non-explanatory parts, and to compose explanations in order to construct chains of consecutive grounding steps.