On a Notion of Relevance Fajar Haifani1,2 , Patrick Koopmann3 , Sophie Tourret1 , and Christoph Weidenbach1 1 Max Planck Institute for Informatics, Saarbrücken Germany 2 Graduate School of Computer Science, Saarbrücken, Germany 3 University of Dresden, Dresden, Germany Abstract. We define a notion of relevance of a clause for proving a par- ticular entailment by the resolution calculus. We think that our notion of relevance is useful for explaining why an entailment holds. A clause is rel- evant if there is no proof of the entailment without it. It is semi-relevant if there is a proof of the entailment using it. It is irrelevant if it is not needed in any proof. By using well-known translations of description log- ics to first-order clause logic, we show that all three notions of relevance are decidable for a number of description logics, including EL and ALC. We provide effective tests for (semi-)relevance. The (semi-)relevance of a DL axiom is defined with respect to the (semi-)relevance of the respective clauses resulting from the translation. 1 Introduction The motivation for this work comes in particular from complexity management in the car industry [22,5]. Here, the set of all buildable cars is described by logical formulas. The formulas encode the available car parts and the rules how to put these parts together on a certain level of abstraction. The different models of the conjunction of the overall set of formulas correspond to all individual buildable cars. A build of a concrete car is performed by proving its entailment with respect to its specification. For example, we may prove that a car with a specific engine, body trim, and suspension can be built. An important question that arises in this context is the overall importance of a rule or a part in a specific car or the space of all cars. This means given some rule or part, we want to know whether there is a car where the part, rule is used for its build. Obviously, if this is not the case, then the part, rule is not used anymore and can be removed from the overall set of logical formulas. The car portfolio permanently changes. Therefore, an inherent part of the engineering is to detect superfluous parts or rules. On the formula level, this question is reflected by our notion of semi-relevance, i.e., is there a proof of an entailment (e.g., a concrete built of a car) using a specific formula (part, rule). Our notion of relevance captures all parts, rules that are mandatory for the existence of a car. This information is very useful for a product car engineer to understand the overall car portfolio and its dependencies. Copyright c 2020 for this paper by its authors. Use permitted under Creative Com- mons License Attribution 4.0 International (CC BY 4.0). The paper is organized as follows: in Section 2 we introduce first-order logic, clausal resolution and translation techniques for description logics to first-order logic up to the expressivity of ALC [9]. Then, in Section 3, we introduce our no- tion of relevance on the basis of first-order clauses. With respect to a DL ontology relevance of an axiom is defined with respect to relevance of the clauses out of the translation. Section 4 develops effective tests for our notions of relevance. Ba- sically, relevance can be decided by resolution and semi-relevance by resolution with a set-of-support strategy. For any logic enjoying the finite model property for which an a priori bound on the size of models can be computed, the test for (semi-)relevance is decidable. Section 5 is devoted to a detailed comparison between our notion of relevance and already existing notions in the DL context. The paper ends with a discussion on directions of further work, in Section 6. 2 Preliminaries We consider a first-order language over a set of variables V and a signature Σ = (Ω, Π) where Ω is an infinite set of function symbols and Π is a finite non-empty set of predicate symbols. Terms, atoms, literals, clauses and formulas are defined in the usual way. We write x, y for variables, a, b for constants, P , Q, R for predicate symbols, t, s for terms, A, B for atoms, L, K for literals and C, D for clauses, all possibly indexed and with or without arguments depending on the context. Given a literal L, comp(L) = ¬A if L = A and comp(L) = A if L = ¬A. As usual, a term not containing any variable is called a ground term. Substitutions σ, λ map variables to terms and are the identity on all but finitely many variables. They are homomorphically extended to terms, literals, clauses, and sets, sequences thereof. Two terms s, t are unifiable if there is a substitution σ with sσ = tσ. A most general substitution with respect to in- stantiation is called a most general unifier, or mgu. The notion of unification is extended to atoms and literals as usual. The resolution calculus consists of the two inference rules resolution and factoring operating on two sets of clauses N and S: Resolution (N, S) ⇒RES (N, S ∪ {(D ∨ C)σ}) if the clauses D ∨ A and ¬B ∨ C are either both in S or one is in S and one is in N and if σ = mgu(A, B) Factoring (N, S ] {C ∨ L ∨ K}) ⇒RES (N, S ∪ {C ∨ L ∨ K} ∪ {(C ∨ L)σ}) if σ = mgu(L, K) The clauses D ∨ A and ¬B ∨ C are the parents of (D ∨ C)σ and the clause C ∨ L ∨ K is the parent of (C ∨ L)σ. Given a set of clauses N , the start state (∅, N ) initializes the above rules for the application of the classical resolution calculus. Given a set of clauses N = N1 ] N2 , the start state (N1 , N2 ) initializes the above rules for the application of the set-of-support (SOS) strategy with set-of-support N2 . 2 Theorem 1 (Soundness and Completeness of Resolution [19,23]). The resolution calculus is sound and refutationally complete. The SOS strategy for an unsatisfiable clause set N = N1 ]N2 is refutationally complete if N1 is satisfiable and N2 is the SOS. A number of description logics can be expressed in first-order logic via a suitable translation. Furthermore, there is a close relationship between certain modal logics and description logics. Table 1, following [9], shows the translation of ALC to first-order logic where in [9] this was shown for a modal logic that can express ALC. We leave out the definitional form from [9] as it is not needed for the examples presented here. A translation of a DL ontology is the conjunction of all translated axioms in the TBox and ABox. Also, we use τ similarly to translate concepts, roles, TBox, ABox, and the whole ontology. Note that, our relevance notion is defined on the clausified axioms. For simplicity, we do not show its clausification in Table 1. The later DL examples have a translation which is almost in clause form. Table 1: ALC First-Order Translation Concepts τ (>, x) = > τ (⊥, x) = ⊥ τ (A, x) = A(x) τ (¬C, x) = ¬τ (C, x) τ (C u D, x) = τ (C, x) ∧ τ (D, x) τ (C t D, x) = τ (C, x) ∨ τ (D, x) τ (∀r.C, x) = ∀y.(τ (r, x, y)) → τ (C, x)) τ (∃r.C, x) = ∃y.(τ (r, x, y) ∧ τ (C, x)) Roles τ (r, x, y) = r(x, y) TBox Axioms τ (C v D) = ∀x.(π(C, x) → τ (D, x)) τ (C ≡ D) = ∀x.(τ (C, x) ↔ τ (D, x)) ABox Axioms τ (C(d)) = τ (C, d) τ (r(d1 , d2 )) = r(d1 , d2 ) 3 A Notion of Relevance A derivation of a clause C from a clause set N is a finite sequence π = [C1 , . . . , Cn ] with Cn = C such that for each Ci ∈ π either: (i) Ci ∈ N or (ii) there is a clause Cj ∈ π, j < i such that Ci is the result of a Factoring inference from Cj or (iii) there are clauses Cj , Ck ∈ π, j < k < i such that Ci is the result of a Resolution inference from Cj and Ck . The derivation π is called connected if in addition every clause is in π is connected, where connectedness in π is defined 3 by Cn = C is connected, and a clause Ci ∈ π is connected if it is the parent of a connected clause. A connected derivation of ⊥ out of N is a refutation (proof ) of N . A derivation π = [C1 , . . . , Cn ] is an SOS derivation from (N, S) if (N, S) ⇒∗RES (N, S 0 ) and Ci ∈ (N ∪ S 0 ) for all i. Definition 2 (Relevance). Given an unsatisfiable set of clauses N , a clause C ∈ N is relevant if for all refutations π of N it holds that C ∈ π. A clause C ∈ N is semi-relevant if there exists a refutation π of N in which C ∈ π. A clause C ∈ N is irrelevant if there is no refutation π of N in which C ∈ π. A different notion of relevance was previously defined in the context of propo- sitional abduction [4]. The authors provide algorithms and complexity results for various abduction settings in the propositional logic context. In addition to the fact that our notion of relevance is defined with respect to first-order clauses, in their context of propositional abduction, if a propositional variable is relevant, it must be satisfiability preserving when added to the theory (clause set). In our case, if a clause C ∈ N is (semi-)relevant, then N is unsatisfiable and N \ {C} may be unsatisfiable as well. With respect to the first-order translation of DL ontologies, see Table 1, the above definition on clauses translates as follows. Whenever we want to prove the entailment of a DL axiom φ from an ontology O, O |= φ, we refute τ (O) ∪ τ (¬φ) via resolution. A DL axiom is then relevant in deriving some entailment, if any refutation of the negation of the entailment after the respective translations contains at least one clause out of the translation of the axiom. A DL axiom is semi-relevant in deriving some entailment, if there is a refutation of the negation of the entailment after the respective translation that contains one clause out of the translation of the axiom. It is irrelevant if there is no such refutation that contains a clause out of the axiom. Note that a relevant DL axiom may translate into several clauses consisting of more than one semi-relevant clauses which are not relevant individually. It may happen that different DL axioms produce the very same clause. In this case we silently assume a labelling of clauses, where all versions of the same clause but different labels are kept [13]. Example 3. As an illustration for our notion of relevance in the DL context, we consider an ALC ontology O = T ∪ A, where T = {LuxurySedan u ∃hasEngine.HighPerformanceEngine v PerformanceCar, LuxurySedan t PerformanceCar v ExecutiveCar} The first concept inclusion says, a luxurious sedan with a high performance engine is a performance car. The second one expresses that luxurious sedans and performance cars are executive cars. In addition, we consider the following 4 ABox: A = { LuxurySedan(mercedes), hasEngine(mercedes, v8), HighPerformanceEngine(v8) PerformanceCar(lamborghini)}. The first-order translation of T according to Table 1 results in ¬LuxurySedan(x) ∨ ¬hasEngine(x, z) ∨ ¬HighPerformanceEngine(z) ∨ PerformanceCar(x) (¬LuxurySedan(x) ∧ ¬PerformanceCar(x)) ∨ ExecutiveCar(x) and we want to prove the entailment O |= ExecutiveCar(mercedes). To find (semi- )relevant axioms for this entailment, we consider ¬ExecutiveCar(mercedes) and the translation of O to first-order logic. A refutation of the obtained formula is the following: π1 = [(1) : ¬LuxurySedan(x) ∨ ¬hasEngine(x, z) ∨ ¬HighPerformanceEngine(z) ∨ PerformanceCar(x), (2) : ¬PerformanceCar(x) ∨ ExecutiveCar(x) (3) : LuxurySedan(mercedes), (4) : hasEngine(mercedes, v8), (5) : HighPerformanceEngine(v8), (6) : ¬LuxurySedan(x) ∨ ¬hasEngine(x, z) ∨ ¬HighPerformanceEngine(z) ∨ ExecutiveCar(x), (7) : ¬hasEngine(mercedes, z) ∨ ¬HighPerformanceEngine(z) ∨ ExecutiveCar(mercedes), (8) : ¬HighPerformanceEngine(v8) ∨ ExecutiveCar(mercedes), (9) : ExecutiveCar(mercedes) (10) : ¬ExecutiveCar(mercedes) (11) : ⊥]. The clauses (1) to (5) are the initial clauses where we simply perform consecutive resolution steps between clause (1) and the other clauses (2) to (5) from τ (A). This will result in the respective clauses (6) to (9). Clause (9) is then refuted by the negated conjecture, (10), resulting in ⊥. Additionally, π2 is the only alternative proof for O |= ExecutiveCar(mercedes) with different initial clauses. π2 = [(1) : ¬LuxurySedan(x) ∨ ExecutiveCar(x) (2) : LuxurySedan(mercedes), (3) : ExecutiveCar(mercedes) (4) : ¬ExecutiveCar(mercedes) (5) : ⊥]. 5 The concept inclusion LuxurySedan t PerformanceCar v ExecutiveCar is there- fore relevant since both proofs must contain at least one clause out of its first- order translation. The ABox axiom LuxurySedan(mercedes) is also relevant. More- over, the TBox axioms LuxurySedan u ∃hasEngine.(HighPerformanceEngine) v PerformanceCar and the ABox axioms LuxurySedan(mercedes), hasEngine(mercedes, v8), and HighPerformanceEngine(v8) are semi-relevant but not relevant. Finally, the ABox axiom PerformanceCar(lamborghini) is irrelevant. 4 Testing for Relevance Our notion of relevance can be effectively tested for a number of description logics, including EL and ALC. Lemma 4 (Relevant Clauses). Given an unsatisfiable set of clauses N , C ∈ N is relevant if and only if N \ {C} is satisfiable. Proof. If N \ {C} is satisfiable then clearly C is contained in any refutation. On the over hand, if C is relevant then, by definition, there cannot be a refutation of N without C. Because of refutational completeness N \ {C} must be satisfiable. The characterization of semi-relevant clauses that are not relevant is more complicated. In the sequel we will prove that given an unsatisfiable clause set N , a clause C ∈ N is semi-relevant if there exists an SOS refutation with set- of-support set {C}, i.e., a derivation (N \ {C}, {C}) ⇒∗RES (N 0 , S 0 ∪ {⊥}). This result is not a consequence of Theorem 1 because if C is semi-relevant but not relevant then N \ {C} is still unsatisfiable. Thus, there is no completeness guarantee for a refutation with set-of-support {C} so far. The idea of our proof is to transform a (non-SOS) refutation using C into an SOS refutation with set-of-support {C}. As an example, consider the unsatisfiable clause set: N = { (1) : ¬B(b, a) ∨ B(x1 , f (x6 )), (2) : ¬B(x3 , f (a)) ∨ A(f (a)), (3) : ¬A(x4 ) ∨ ¬B(b, x4 ), (4) : B(b, x2 ) ∨ C(x2 ), (5) : ¬C(x5 )}, where the clause (1) is semi-relevant but not relevant. We attach unique numbers to clauses for reference and indicate resolution (factoring) steps by writing nRm (respectively nF ) meaning that the clause is a result of a resolvent between clause n and clause m (respectively a factor out of clause n). A refutation including clause (1) is: π1 = [ (2), (3), 2R3 (6) : ¬B(x3 , f (a)) ∨ ¬B(b, f (a)), 6F (7) : ¬B(b, f (a)), (1), (4), 1R4 (8) : B(x1 , f (x6 )) ∨ C(a), 8R7 (9) : C(a), (5), 9R5 (10) : ⊥], where the inference 1R4 (8) is an SOS step with set-of-support {¬B(b, a) ∨ B(x1 , f (x6 ))} while the inference 2R3 (6) and 6F (7) are not SOS steps. The 6 refutation is depicted in the graph in Figure 1 where shaded clauses mark clauses contained in an respective SOS when started with SOS {(1)}. (2):¬B(x3 ,f (a)) ∨ A(f (a)) (3):¬A(x4 ) ∨ ¬B(b,x4 ) {x4 7→ f (a)} (1):¬B(b,a) ∨ B(x1 ,f (x6 )) (4):B(b,x2 ) ∨ C(x2 ) (6):¬B(x3 ,f (a)) ∨ ¬B(b,f (a)) {x2 7→ a} {x3 7→ b} (8):B(x1 ,f (x6 )) ∨ C(a) (7):¬B(b,f (a)) {x1 7→ b, x6 7→ a} (5):¬C(x5 ) (9):C(a) {x5 7→ a} (10):⊥ Fig. 1. Non-SOS Refutation with ¬B(b, a) ∨ B(x1 , f (x6 )) Tracing back the literals in the original clause set resolved by B(x1 , f (x6 )) out of clause (8), the idea of our completeness proof is to start with these steps; for the example, resolving B(x1 , f (x6 )) in clause (1) with the appropriate literals from clauses (2) and (3). This then already leads to the following SOS refutation π2 = [ (1), (4), 1R4(8) : B(x1 , f (x6 )) ∨ C(a), (2), 2R8(11) : A(f (a)) ∨ C(a), 3R8(12) : ¬A(f (x6 )) ∨ C(a), 11R12(13) : C(a) ∨ C(a), 13F (14) : C(a), (5), 14R5(15) : ⊥]. also depicted in the following graph, where shaded clauses mark clauses contained in the SOS. (1):¬B(b,a) ∨ B(x1 ,f (x6 )) (4):B(b,x2 ) ∨ C(x2 ) {x2 7→ a} (2):¬B(x3 ,f (a)) ∨ A(f (a)) (8):B(x1 ,f (x6 )) ∨ C(a)) (3):¬A(x4 ) ∨ ¬B(b,x4 ) {x3 7→ x1 } {x6 7→ a} {x1 7→ b} {x4 7→ f (x6 )} (11):A(f (a)) ∨ C(a) (12):¬A(f (x6 )) ∨ C(a) {x6 7→ a} (13):C(a) ∨ C(a) (5):¬C(x5 ) (14):C(a) {x5 7→ a} (15):⊥ Fig. 2. SOS refutation with ¬B(b, a) ∨ B(x1 , f (x6 )) 7 The transformation from the non-SOS refutation π1 to the SOS refutation of π2 is exactly the idea of the proof below of Theorem 5. Clause (1) is not relevant, because there is also a refutation without it: π3 = [ (4), (5), 4R5(16) : B(b, x2 ), (2), 2R16(17) : A(f (a)), (3), 3R17(18) : ¬B(b, f (a)), 16R18(19) : ⊥] Theorem 5 (Semi-Relevance Test). Given an unsatisfiable clause set N ] {C}, the clause C is semi-relevant if and only if (N, {C}) ⇒∗RES (N, S 0 ∪ {⊥}) via SOS. Proof. (Sketch) The backward implication holds by definition. To prove the for- ward implication let us assume the clause C is semi-relevant. We need to show that (N, {C}) ⇒∗RES (N, S 0 ∪ {⊥}) via SOS. By definition, there is a resolution refutation π (without SOS) containing C. If π is also an SOS refutation we are done. If not, we subsequently transform π into an SOS proof via an inductive argument. For simplicity and without loss of generality, we assume that π has a tree structure, i.e., each clause is used exactly once in the refutation, and all clauses taken from N ] {C} are variable disjoint. Therefore, there is a unique overall substitution σ such that πσ is also a refutation where all mgus are iden- tities. The underlying well-founded ordering for the inductive argument is the multiset of all distances (number of steps) from any clause C ∈ π to ⊥ where C is not generated by the SOS strategy. Now we pick a clause nRm (l) : D in π, where n, m < l, l minimal, and m is contained in the SOS, but clause n is not in N and has not been generated by an SOS derivation. Let L be the literal of m resolved upon. Then we trace back comp(L) in π to the clauses out of N eventually gen- erating the clause n. Now we resolve all these clauses first with variable-disjoint copies of m on comp(L). For each copy, σ is extended accordingly, i.e., the fresh extra variables are mapped to the same terms as their originals. Then we redo the derivation of n following exactly the steps out of π, resulting in π 0 . This derivation will then generate the clause D via SOS, possibly after some extra factoring steps. Thus π 0 gets strictly smaller with respect to the well-founded above defined measure. This transformation is possible, because any mgu occur- ring in π or in π 0 can always be instantiated to σ. Our transformation does not change the starting overall contradicting substitution σ. Corollary 6 ((Semi)-Relevance Decidability). If resolution is a decision procedure for some class of clause sets, then (semi-)relevance is decidable. Many description logics enjoy the finite model property, where the relevant finite model for some clause set can be explicitly a priori generated [9]. In this case the logics enjoy the bounded model property. In particular, if resolution is not a decision procedure for the logic under consideration, an explicit bound on the Herbrand universe is needed. In [9], the bounded model property of EL, ALC and other logics is used to provide for a translation-based decision procedure for these logics. In general, this approach can however be used for many description logic that have the finite model property, including more expressive description logics such as SHOI. 8 Lemma 7 ((Semi)-Relevance Decidability in Description Logics). For ontologies in a DL that enjoys the bounded model property, (semi-)relevance of an axiom for a given property is decidable. Proof. We translate both the (negated) property and the ontology to first-order logic. For relevance, we first check satisfiability of the resulting clause set without the clauses from the axiom via resolution using the bounded model property. This terminates because we only have to consider terms out of the finite Herbrand base generated by these logics [9]. If the clause set is unsatisfiable, the axiom is either irrelevant or semi-relevant but not relevant. If this clause set is satisfiable the axiom is either relevant or irrelevant because then semi-relevance implies relevance. In both cases testing for semi-relevance provides the final classification of the axiom. To test for semi-relevance, we perform an SOS resolution proof attempt where the set of support contains the clauses corresponding to the axiom. If this results in a refutation, the axiom is semi-relevant or relevant for the property depending on the previous test, otherwise it is irrelevant. All resolution proof attempts terminate, because they can be stopped once the generated terms exceed the expected bounded Herbrand universe. Example 8. We illustrate how the semi-relevant clauses may be lifted to semi- relevance on TBox axioms. Consider the ontology O = T ∪ A where: T = {A v B u F, (B u C) t G v D, B t D v E}, A = {A(a), C(a)}, and consider the entailment O |= E(a). The TBox T is translated into: τ (A v B u F ) = {¬A(x) ∨ B(x), ¬A(x) ∨ F (x)}, τ ((B u C) t G v D) = {¬B(x) ∨ ¬C(x) ∨ D(x), ¬G(x) ∨ D(x)}, τ (B t D v E) = {¬B(x) ∨ E(x), ¬D(x) ∨ E(x)}. For the above clauses, the bounded Herbrand universe consists of a single ele- ment: {a}. Either this clause set has a model with domain {a} or it does not have a model at all. Furthermore, for this particular clause set resolution is al- ready a decision procedure. Then the axioms A v B u F and B t D v E are relevant because any refutation of E(a) will always contain at least one clauses from τ (A v B u F ) and τ (B t D v E) respectively. Moreover (B u C) t G v D is semi-relevant because we can find a refutation where either ¬B(x)∨¬C(x)∨D(x) or ¬G(x) ∨ D(x) do not exist. Note that here, relevance in clausal form differs when it is lifted to DL axiom. The axiom BtD v E is relevant but its translation consists of only semi-relevant (but not relevant) clauses. 9 5 Relations to Other Notions in Description Logics and Beyond The notions relevant axioms and semi-relevant axioms are related to two prob- lems in description logics: justifications and repairs. Given an ontology O and an axiom α s.t. O |= α, a justification for O |= α is a subset-minimal set J ⊆ O s.t. J |= α [10,20]. A generalisation of justifications is the concept of a MinA [1], which denotes a minimal axiom set preserving some given property. The process of computing justifications and MinAs is known as axiom pinpointing. Justifi- cations are classically used for explaining entailments observed by a reasoner, for which they are used for example in the ontology editor Protégé [14]. Axioms that occur in at least one justification have also been studied under the name MinA-relevant axioms [1,17]. In addition to MinA-relevancy, they even study a corresponding counting problem #minA-relevance which is to count the number of MinAs in which a given axiom occurs. MinA-relevant axioms corre- spond to the case where this count is 1 or more, and MinA-irrelevant axioms are those whose count is 0, but the count can give a more detailed account on the relevance of axioms. If the count correspond to the number of MinAs for the entailment (the corresponding counting problem #minA is also studied in [17]), then it occurs in every justification. If an axiom occurs in a justification for α, in the translation into first order logic, the axiom will be involved in some proof for O |= α. Thus, every axiom in a justification is semi-relevant for this entailment. One may be tempted to identify MinA-relevant axioms with semi-relevant ones. Though in most cases, these notions will coincide, it is in fact possible for an axiom to be semi-relevant even if it does not occur in any justification, as the following example shows. Example 9. Consider the ontology O = T ∪ A consisting of the TBox: T = {A v B, B u C v D, B t D v E} and the ABox A = {A(a), C(a)}; and consider the entailment O |= E(a). There is only one justification for this entailment, namely {A v B, B t D v E, A(a)}, so that only those axioms are MinA-relevant for E(a). In contrast, all axioms in the ontology are semi-relevant for E(a). A first proof in first-order logic uses, in addition to the negation of E(a) the axioms A(a), A v B and B t D v E: [A(a), ¬A(x) ∨ B(x), B(a), ¬B(x) ∨ E(x), E(a), ¬E(a), ⊥]. A second proof also uses A(a), A v B and B t D v E, but additionally includes C(a) and B u C v D: [A(a), ¬A(x) ∨ B(x), B(a), ¬B(x) ∨ ¬C(x) ∨ D(x), ¬C(a) ∨ D(a), C(a), D(a), ¬D(x) ∨ E(x), E(a), ¬E(a), ⊥]. As the example illustrates, our notion of relevance captures connections be- tween axioms and entailments that are not captured by the classical notion of justification or MinA-relevance. 10 The notion of relevant axioms is also related to what has been studied in the field of propositional satisfiability under the name of lean kernels [11,12]: given an unsatisfiable set F of propositional clauses, the lean kernel Na (F ) ⊆ N consists exactly of those clauses that are involved in at least one refutation proof of N in the resolution calculus, and thus, in our terminology, the set of semi- relevant clauses. This notion has been extended to description logics in [16], not only considering resolution as an inference procedure, but even arbitrary consequence-based reasoning procedures. [16] also discuss a generalisation of lean kernels called MinA-preserving module: given an ontology O and an axiom α, a MinA-preserving module for α in O is a subset M ⊆ O s.t. every justification for O |= α is a subset of M. There is no minimality requirement, that is, a MinA- preserving module may contain axioms that do not occur in any justification. Because every axiom in a justification is also semi-relevant, the set of all semi- relevant axioms is also a MinA-preserving module. However, as we illustrated with the previous example, the set of semi-relevant axioms may capture more relations than a MinA-preserving module. As semi-relevance is determined on the level of first-order clauses, there is also a connection to laconic justifications [7]. A laconic justification departs from a justification in that it does not have to be a subset of the original ontology, but may contain axioms that are the result of simplifying axioms in a justification, for instance by removing conjuncts and disjuncts that are irrelevant for the entailment. When considering the set of semi-relevant clauses instead of axioms, we obtain a similar level of precision as with laconic justifications. Example 10. Consider the ontology: O = {A v B u C, D t B v E}. The whole ontology is a justification for O |= A v E. However, the concepts C and D are superfluous, i.e., they are not needed for the entailment, so that the axioms would be simplified for the laconic justification. The laconic justification is thus J = {A v B, B v E}. Now consider the first-order translation of O. ¬A(x) ∨ B(x), ¬A(x) ∨ C(x), ¬D(x) ∨ E(x), ¬B(x) ∨ E(x) (1) Here, our notion would categorize {¬A(x) ∨ B(x), ¬B(x) ∨ E(x)} as relevant, while the clauses {¬A(x)∨C(x), ¬D(x)∨E(x)} would be irrelevant. The relevant clauses correspond to the axioms in the laconic justification. It remains to check whether this always holds or not, which we leave as future work. While axioms in justifications correspond to semi-relevant axioms, an axiom that occurs in all justifications corresponds to a relevant axiom. When exhibiting justifications, it is helpful to understand whether they occur only in one justi- fication or in several. This is for instance reflected in the visual presentation of justifications in Protégé [15], that indicates for each axiom in a justification in how many justifications it is included, or whether it is included in every justifi- cation. 11 Another important connection however is from relevant axioms to repairs. In ontology repair, the aim is to remove an unwanted entailment from an ontology. Specifically, a repair for an entailment O |= α is a subset-minimal set R ⊆ O s.t. O \ R 6|= α [8]. A repair for O |= α always contains one axiom from every justification for O |= α, a fact that is used in the method for computing repairs based on Reiter’s Minimal Hitting Set Algorithm [18]. It is not hard to see that a relevant axiom corresponds to the special case of a repair consisting of exactly one element. Rather than computing these repairs through the detour of justifications, our method provides a way of computing these repairs directly. Two final formalisms worth mentioning are provenance semirings and axiom pinpointing formulas, as they both are often used to link inferences to entail- ments. Given an entailment α and an ontology O, a pinpointing formula is a monotone propositional formula φ over the axioms in O (as propositional sym- bols) s.t. every model of the formula entails α, and the set of justifications corresponds exactly to the set of minimal models of φ. Thus, pinpointing for- mulas can be used to generate justifications, but also have other applications. Similar to our approach for computing semi-relevant axioms, there are methods for computing pinpointing formulas by intercepting reasoning procedures, as for instance done for EL in [2]. This idea of pinpointing formulas is very related to that of provenance semirings from the field of database access [6], recently investigated also in the context of DLs [3]. Here the idea is to compute a for- mula, called provenance polynomial, that links a query result or entailment to the database entries that are involved in computing the query. 6 Conclusion We introduced the notions of relevance and semi-relevance in first-order logic, showed their effectiveness and discussed their relationship to existing notions known in the DL context. Our notion of relevance adds new aspects in under- standing an ontology to the related DL notions of justifications and repairs. In particular, semi-relevant clauses appear to be particularly connected to laconic justifications and the computation of relevant axioms offers an alternative to existing repair methods. The test procedure suggested in Section 4 relying on an explicit finite domain can be inefficient. It would be desirable to use the original first-order decision pro- cedures, e.g., ordered resolution [21] for the (semi-)relevance tests. For relevance this can be obviously done. For semi-relevance this needs an extra argument, because the SOS strategy is not a priori compatible with ordered resolution. However, we believe that an extended concept of saturation can lead to a com- plete SOS procedure for ordered resolution. In any case, the design of an efficient semi-relevancy detection algorithm is the next considered step in this work. Acknowledgments: We thank our reviewers for their valuable comments. This work was funded by DFG grant 389792660 as part of TRR 248 “Foundations of Perspicuous Software Systems”. 12 References 1. Baader, F., Peñaloza, R.: Axiom pinpointing in general tableaux. J. Log. Com- put. 20(1), 5–34 (2010). https://doi.org/10.1093/logcom/exn058, https://doi. org/10.1093/logcom/exn058 2. Baader, F., Peñaloza, R., Suntisrivaraporn, B.: Pinpointing in the description logic EL+ . In: Hertzberg, J., Beetz, M., Englert, R. (eds.) KI 2007: Advances in Artifi- cial Intelligence, 30th Annual German Conference on AI, KI 2007, Osnabrück, Ger- many, September 10-13, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4667, pp. 52–67. Springer (2007). https://doi.org/10.1007/978-3-540-74565- 5 7, https://doi.org/10.1007/978-3-540-74565-5_7 3. Bourgaux, C., Ozaki, A.: Querying attributed dl-lite ontologies using provenance semirings. In: The Thirty-Third AAAI Conference on Ar- tificial Intelligence, AAAI 2019. pp. 2719–2726. AAAI Press (2019). https://doi.org/10.1609/aaai.v33i01.33012719, https://doi.org/10.1609/ aaai.v33i01.33012719 4. Eiter, T., Gottlob, G.: The complexity of logic-based abduction. Journal of the ACM 42(1), 3–42 (1995) 5. Fetzer, C., Weidenbach, C., Wischnewski, P.: Compliance, functional safety and fault detection by formal methods. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemi- nation, Applications - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II. Lecture Notes in Computer Science, vol. 9953, pp. 626–632 (2016) 6. Green, T.J., Karvounarakis, G., Tannen, V.: Provenance semirings. In: Libkin, L. (ed.) Proceedings of the Twenty-Sixth ACM SIGACT-SIGMOD-SIGART Sym- posium on Principles of Database Systems, June 11-13, 2007, Beijing, China. pp. 31–40. ACM (2007). https://doi.org/10.1145/1265530.1265535, https://doi.org/ 10.1145/1265530.1265535 7. Horridge, M., Parsia, B., Sattler, U.: Laconic and precise justifications in OWL. In: The Semantic Web - ISWC 2008, 7th International Semantic Web Confer- ence, ISWC 2008, Karlsruhe, Germany, October 26-30, 2008. Proceedings. pp. 323– 338 (2008). https://doi.org/10.1007/978-3-540-88564-1 21, https://doi.org/10. 1007/978-3-540-88564-1_21 8. Horridge, M., Parsia, B., Sattler, U.: Explaining inconsistencies in OWL on- tologies. In: Godo, L., Pugliese, A. (eds.) Scalable Uncertainty Management, Third International Conference, SUM 2009. Lecture Notes in Computer Science, vol. 5785, pp. 124–137. Springer (2009). https://doi.org/10.1007/978-3-642-04388- 8 11, https://doi.org/10.1007/978-3-642-04388-8_11 9. Hustadt, U., Schmidt, R.A.: Using resolution for testing modal satisfiability and building models. Journal of Automed Reasoning 28(2), 205–232 (2002) 10. Kalyanpur, A., Parsia, B., Horridge, M., Sirin, E.: Finding all justifications of OWL DL entailments. In: Aberer, K., Choi, K., Noy, N.F., Allemang, D., Lee, K., Nixon, L.J.B., Golbeck, J., Mika, P., Maynard, D., Mizoguchi, R., Schreiber, G., Cudré-Mauroux, P. (eds.) The Semantic Web, 6th International Semantic Web Conference, 2nd Asian Semantic Web Conference, ISWC 2007 + ASWC 2007, Busan, Korea, November 11-15, 2007. Lecture Notes in Computer Science, vol. 4825, pp. 267–280. Springer (2007). https://doi.org/10.1007/978-3-540-76298- 0 20, https://doi.org/10.1007/978-3-540-76298-0_20 13 11. Kleine Büning, H., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiabil- ity, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 339–401. IOS Press (2009). https://doi.org/10.3233/978-1-58603-929-5-339, https://doi.org/ 10.3233/978-1-58603-929-5-339 12. Kullmann, O.: Investigations on autark assignments. Discret. Appl. Math. 107(1- 3), 99–137 (2000). https://doi.org/10.1016/S0166-218X(00)00262-6, https://doi. org/10.1016/S0166-218X(00)00262-6 13. Lev-Ami, T., Weidenbach, C., Reps, T.W., Sagiv, M.: Labelled clauses. In: Pfen- ning, F. (ed.) Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings. LNCS, vol. 4603, pp. 311–327. Springer (2007) 14. Musen, M.A.: The protégé project: a look back and a look forward. AI Matters 1(4), 4–12 (2015) 15. Musen, M.A.: The protégé project: a look back and a look forward. AI Matters 1(4), 4–12 (2015). https://doi.org/10.1145/2757001.2757003, https://doi.org/ 10.1145/2757001.2757003 16. Peñaloza, R., Mencı́a, C., Ignatiev, A., Marques-Silva, J.: Lean kernels in descrip- tion logics. In: Blomqvist, E., Maynard, D., Gangemi, A., Hoekstra, R., Hitzler, P., Hartig, O. (eds.) The Semantic Web - 14th International Conference, ESWC 2017, Portorož, Slovenia, May 28 - June 1, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10249, pp. 518–533 (2017). https://doi.org/10.1007/978-3- 319-58068-5 32, https://doi.org/10.1007/978-3-319-58068-5_32 17. Peñaloza, R., Sertkaya, B.: Understanding the complexity of axiom pin- pointing in lightweight description logics. Artif. Intell. 250, 80–104 (2017). https://doi.org/10.1016/j.artint.2017.06.002, https://doi.org/10.1016/j. artint.2017.06.002 18. Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57– 95 (1987). https://doi.org/10.1016/0004-3702(87)90062-2, https://doi.org/10. 1016/0004-3702(87)90062-2 19. Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965). https://doi.org/10.1145/321250.321253, http://doi. acm.org/10.1145/321250.321253 20. Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description logic terminologies. In: Gottlob, G., Walsh, T. (eds.) IJCAI-03, Pro- ceedings of the Eighteenth International Joint Conference on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003. pp. 355–362. Morgan Kaufmann (2003), http://ijcai.org/Proceedings/03/Papers/053.pdf 21. Schmidt, R.A.: Decidability by resolution for propositional modal logics. J. Au- tom. Reasoning 22(4), 379–396 (1999). https://doi.org/10.1023/A:1006043519663, https://doi.org/10.1023/A:1006043519663 22. Sinz, C., Kaiser, A., Küchlin, W.: Formal methods for the valida- tion of automotive product configuration data. AI EDAM 17(1), 75–97 (2003). https://doi.org/10.1017/S0890060403171065, https://doi.org/10.1017/ S0890060403171065 23. Wos, L., Robinson, G.A., Carson, D.F.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12(4), 536– 541 (1965). https://doi.org/10.1145/321296.321302, https://doi.org/10.1145/ 321296.321302 14