Decisions made by an automated system, especially in sensitive domains involving interaction with humans, must be explained. Such explanations should be transparent and detailed enough to verify the work of the system. In this way, a user does not have to trust the manufacturers and developers implicitly, but can verify that the system indeed does what it is supposed to do. One way to explain logical reasoning is by providing a proof for the established entailments, composed of individual, easy to understand reasoning steps leading from the asserted knowledge to the inferred conclusion. Since such proofs may be arbitrarily complex, ideally we would like to pick a proof that is easiest to understand. This theoretical paper investigates the complexity of finding proofs of a given quality among all possible alternative proofs. The quality of a proof is determined by a proof measure m and an upper bound q that filters out bad proofs w.r.t. the measure. That is, we want to decide the existence of a proof P with m(P) ≤ q. Our analysis is based on the notion of a deriver, which generates a so-called derivation structure consisting of possible proof steps, from which all proofs of the given consequence can be constructed. This structure can be thought of as containing all possible instantiations of a specific set of inference rules, for some specific KB K and entailment η to be proven. Practical inference systems often restrict the shape of derived axioms, e.g. to be in a certain normal form or to use only subconcepts from the input, thus giving a bound on the number of steps in a derivation structure based on K and η. Based on this bound, we can distinguish polynomial and exponential derivers, examples of which are consequence-based reasoners for the DLs EL [3, 9] and ELI [4, 8]. The complexity of generating the derivation structure is not considered part of the complexity of finding good proofs since we do not want to be limited by the choice of the underlying logic or the inference rule set. In many cases, a derivation structure can also be generated in a goal-oriented way, without having to fully explore all possible rule instances. Table 1 gives an overview of known and new results, going from general classes of measures to specific cases. This paper extends the results of [1,2], where
Alrabbaa, Baader, Borgwardt, Koopmann, Kovtunova
we had established results concerning some proof measures m with respect to
polynomial/exponential derivers with both unary and binary encoding of the
upper bound q. In particular, in our first work in this direction [
In this paper, we extend the latter line of research by providing a more
general notion of measures, monotone recursive Φ-measures, which also allow to
measure the depth and logarithmic depth of a proof. We prove that every local
Ψ-measure is a monotone recursive Φ-measure, but not vice versa. Therefore,
in this paper we improve the previous results from [
In future work, we plan to investigate more fine-grained measures of proof
quality, inspired by the weighted justification measure of [