We discuss explanations in Description Logics (DLs), a family of logics used for knowledge representation. Initial work on explaining consequences for DLs had focused on justifications, which are minimal subsets of axioms that entail the consequence. More recently, it was proposed that proofs can provide more detailed information about why a consequence follows. Moreover, several measures have been proposed to estimate the comprehensibility of justifications and proofs, for example, their size or the complexity of logical expressions. In this paper, we analyze the connection between these measures, e.g. whether small justifications necessarily give rise to small proofs. We use a dataset of DL proofs that was constructed last year based on the ontologies of the OWL Reasoner Evaluation 2015. We find that, in general, less complex justifications indeed correspond to less complex proofs, and discuss some exceptions to this rule.

It is well known that mathematics students have to be able to understand and prove theorems. From our experience we know that engineering students should also be able to do the same, since a good theoretical knowledge of mathematics is essential for solving practical problems and constructing models. Proving theorems gives students a much better understanding of the subject, and helps them to develop mathematical thinking. The proof of a theorem consists of a logical chain of steps. Students should understand the need and the legitimacy of every step. Moreover, they have to comprehend the reasoning behind the order of the chain’s steps. For our research students were provided with proofs whose steps were either written in a random order or had missing parts. Students were asked to solve the \"puzzle\" – find the correct logical chain or complete the proof. These \"puzzles\" were meant to discourage students from simply memorizing the proof of a theorem. By using our examples students were encouraged to think independently and came to improve their understanding of the subject.

It is well known that mathematics students have to be able to understand and prove theorems. From our experience we know that engineering students should also be able to do the same, since a good theoretical knowledge of mathematics is essential for solving practical problems and constructing models. Proving theorems gives students a much better understanding of the subject, and helps them to develop mathematical thinking. The proof of a theorem consists of a logical chain of steps. Students should understand the need and the legitimacy of every step. Moreover, they have to comprehend the reasoning behind the order of the chain’s steps. For our research students were provided with proofs whose steps were either written in a random order or had missing parts. Students were asked to solve the \"puzzle\" – find the correct logical chain or complete the proof. These \"puzzles\" were meant to discourage students from simply memorizing the proof of a theorem. By using our examples students were encouraged to think independently and came to improve their understanding of the subject.

Diese Arbeit nutzt und verfeinert Methoden der Komplexitätstheorie, um mit diesen die Komplexität dünner Instanzen zu untersuchen. Dazu gehören etwa Graphen mit wenigen Kanten oder Formeln mit wenigen Bedingungen beschränkter Weite. Dabei ergeben sich zwei natürliche Fragestellungen: (a) Gibt es einen effizienten Algorithmus, der beliebige Instanzen eines NP-schweren Problems auf äquivalente, dünne Instanzen reduziert? (b) Gibt es einen Algorithmus, der dünne Instanzen NP-schwerer Probleme bedeutend schneller löst als allgemeine Instanzen gelöst werden können? Wir formalisieren diese Fragen für verschiedene Probleme und zeigen, dass positive Antworten jeweils zu komplexitätstheoretischen Konsequenzen führen, die als unwahrscheinlich gelten. Frage (a) wird als Kommunikation modelliert, in der zwei Akteure kooperativ eine NP-schwere Sprache entscheiden möchten und dabei möglichst wenig kommunizieren. Unter der komplexitätstheoretischen Annahme, dass coNP keine Teilmenge von NP/poly ist, erhalten wir aus unseren Ergebnissen erstaunlich scharfe untere Schranken für interessante Parameter aus verschiedenen Teilgebieten der theoretischen Informatik. Im Speziellen betrifft das die Ausdünnung von Formeln, die Kernelisierung aus der parameterisierten Komplexitätstheorie, die verlustbehaftete Kompression von Entscheidungsproblemen, und die Theorie der probabilistisch verifizierbaren Beweise. Wir untersuchen Fragestellung (b) anhand der Exponentialzeitkomplexität von Zählproblemen. Unter (Varianten) der bekannten Exponentialzeithypothese (ETH) erhalten wir exponentielle untere Schranken für wichtige #P-schwere Probleme: das Berechnen der Zahl der erfüllenden Belegungen einer 2-KNF Formel, das Berechnen der Zahl aller unabhängigen Mengen in einem Graphen, das Berechnen der Permanente einer Matrix mit Einträgen 0 und 1, das Auswerten des Tuttepolynoms an festen Punkten. / In this thesis, we use and refine methods of computational complexity theory to analyze the complexity of sparse instances, such as graphs with few edges or formulas with few constraints of bounded width. Two natural questions arise in this context: (a) Is there an efficient algorithm that reduces arbitrary instances of an NP-hard problem to equivalent, sparse instances? (b) Is there an algorithm that solves sparse instances of an NP-hard problem significantly faster than general instances can be solved? We formalize these questions for different problems and show that positive answers for these formalizations would lead to consequences in complexity theory that are considered unlikely. Question (a) is modeled by a communication process, in which two players want to cooperatively decide an NP-hard language and at the same time communicate as few as possible. Under the complexity-theoretic hypothesis that coNP is not in NP/poly, our results imply surprisingly tight lower bounds for parameters of interest in several areas, namely sparsification, kernelization in parameterized complexity, lossy compression, and probabilistically checkable proofs. We study the question (b) for counting problems in the exponential time setting. Assuming (variants of) the exponential time hypothesis (ETH), we obtain asymptotically tight, exponential lower bounds for well-studied #P-hard problems: Computing the number of satisfying assignments of a 2-CNF formula, computing the number of all independent sets in a graph, computing the permanent of a matrix with entries 0 and 1, evaluating the Tutte polynomial at fixed evaluation points.