We de ne a notion of relevance of a clause for proving a particular entailment by the resolution calculus. We think that our notion of relevance is useful for explaining why an entailment holds. A clause is relevant 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 logics to rst-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 e ective tests for (semi-)relevance. The (semi-)relevance of a DL axiom is de ned with respect to the (semi-)relevance of the respective clauses resulting from the translation.
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 di erent 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 speci cation. For example, we may prove that a car with a speci c 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 speci c 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 super uous parts or rules. On the formula level, this question is re ected 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 speci c 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.
The paper is organized as follows: in Section 2 we introduce rst-order logic, clausal resolution and translation techniques for description logics to rst-order logic up to the expressivity of ALC [9]. Then, in Section 3, we introduce our notion of relevance on the basis of rst-order clauses. With respect to a DL ontology relevance of an axiom is de ned with respect to relevance of the clauses out of the translation. Section 4 develops e ective tests for our notions of relevance. Basically, relevance can be decided by resolution and semi-relevance by resolution with a set-of-support strategy. For any logic enjoying the nite 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
We consider a rst-order language over a set of variables V and a signature = ( ; ) where is an in nite set of function symbols and is a nite non-empty set of predicate symbols. Terms, atoms, literals, clauses and formulas are de ned 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 nitely many variables. They are homomorphically extended to terms, literals, clauses, and sets, sequences thereof. Two terms s; t are uni able if there is a substitution with s = t . A most general substitution with respect to instantiation is called a most general uni er, or mgu. The notion of uni cation 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 [ f(D _ C) g) 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 ] fC _ L _ Kg) )RES (N; S [ fC _ L _ Kg [ f(C _ L) g) 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. Theorem 1 (Soundness and Completeness of Resolution [19,23]). The resolution calculus is sound and refutationally complete. The SOS strategy for an unsatis able clause set N = N1 ]N2 is refutationally complete if N1 is satis able and N2 is the SOS.
A number of description logics can be expressed in rst-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 rst-order logic where in [9] this was shown for a modal logic that can express ALC. We leave out the de nitional 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 de ned on the clausi ed axioms. For simplicity, we do not show its clausi cation in Table 1. The later DL examples have a translation which is almost in clause form.
(9r:C; x) = 9y:( (r; x; y) ^ (C; x)) (r; x; y) = r(x; y) (C v D) = 8x:( (C; x) ! (C
D) = 8x:( (C; x) $
(C(d)) = (C; d) (r(d1; d2)) = r(d1; d2) (C; x))
Roles
(D; x)) (D; x))
ABox Axioms 3
A derivation of a clause C from a clause set N is a nite sequence = [C1; : : : ; Cn] with Cn = C such that for each Ci 2 either: (i) Ci 2 N or (ii) there is a clause Cj 2 , j < i such that Ci is the result of a Factoring inference from Cj or (iii) there are clauses Cj ; Ck 2 , 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 de ned by Cn = C is connected, and a clause Ci 2 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; S0) and Ci 2 (N [ S0) for all i.
De nition 2 (Relevance). Given an unsatis able set of clauses N , a clause C 2 N is relevant if for all refutations of N it holds that C 2 . A clause C 2 N is semi-relevant if there exists a refutation of N in which C 2 . A clause C 2 N is irrelevant if there is no refutation of N in which C 2 .
A di erent notion of relevance was previously de ned in the context of propositional 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 de ned with respect to rst-order clauses, in their context of propositional abduction, if a propositional variable is relevant, it must be satis ability preserving when added to the theory (clause set). In our case, if a clause C 2 N is (semi-)relevant, then N is unsatis able and N n fCg may be unsatis able as well.
With respect to the rst-order translation of DL ontologies, see Table 1, the above de nition on clauses translates as follows. Whenever we want to prove the entailment of a DL axiom from an ontology O, O j= , 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 di erent 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 di erent 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 = fLuxurySedan u 9hasEngine:HighPerformanceEngine v PerformanceCar;
The rst 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 HighPerformanceEngine(v8)
The rst-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 j= ExecutiveCar(mercedes). To nd
(semi)relevant axioms for this entailment, we consider :ExecutiveCar(mercedes) and
the translation of O to rst-order logic. A refutation of the obtained formula is
the following:
1 = [(
PerformanceCar(x);
(
ExecutiveCar(x);
(
ExecutiveCar(mercedes);
(
fore relevant since both proofs must contain at least one clause out of its rstorder translation. The ABox axiom LuxurySedan(mercedes) is also relevant. Moreover, the TBox axioms LuxurySedan u 9hasEngine:(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
Our notion of relevance can be e ectively tested for a number of description logics, including E L and ALC.
Lemma 4 (Relevant Clauses). Given an unsatis able set of clauses N , C 2 N is relevant if and only if N n fCg is satis able.
Proof. If N n fCg is satis able then clearly C is contained in any refutation. On the over hand, if C is relevant then, by de nition, there cannot be a refutation of N without C. Because of refutational completeness N n fCg must be satis able.
The characterization of semi-relevant clauses that are not relevant is more complicated. In the sequel we will prove that given an unsatis able clause set N , a clause C 2 N is semi-relevant if there exists an SOS refutation with setof-support set fCg, i.e., a derivation (N n fCg; fCg) )RES (N 0; S0 [ f?g). This result is not a consequence of Theorem 1 because if C is semi-relevant but not relevant then N n fCg is still unsatis able. Thus, there is no completeness guarantee for a refutation with set-of-support fCg so far. The idea of our proof is to transform a (non-SOS) refutation using C into an SOS refutation with set-of-support fCg.
As an example, consider the unsatis able clause set:
N = f (
fx2 7! ag
(
(
fx4 7! f(a)g
(
fx3 7! bg
(
Tracing back the literals in the original clause set resolved by B(x1; f (x6))
out of clause (
(
fx6 7! ag
(
(
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 (
(
Proof. (Sketch) The backward implication holds by de nition. To prove the forward implication let us assume the clause C is semi-relevant. We need to show that (N; fCg) )RES (N; S0 [ f?g) via SOS. By de nition, 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 ] fCg are variable disjoint. Therefore, there is a unique overall substitution such that is also a refutation where all mgus are identities. The underlying well-founded ordering for the inductive argument is the multiset of all distances (number of steps) from any clause C 2 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 generating the clause n. Now we resolve all these clauses rst 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 de ned measure. This transformation is possible, because any mgu occurring 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 nite model property, where the relevant nite 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 E L, 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 nite model property, including more expressive description logics such as SHOI. 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 rst-order logic. For relevance, we rst check satis ability 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 nite Herbrand base generated by these logics [9]. If the clause set is unsatis able, the axiom is either irrelevant or semi-relevant but not relevant. If this clause set is satis able the axiom is either relevant or irrelevant because then semi-relevance implies relevance. In both cases testing for semi-relevance provides the nal classi cation 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 semirelevance on TBox axioms. Consider the ontology O = T [ A where: T = fA v B u F; (B u C) t G v D; B t D v Eg;
A = fA(a); C(a)g; and consider the entailment O j= E(a). The TBox T is translated into: (A v B u F ) = f:A(x) _ B(x); :A(x) _ F (x)g; ((B u C) t G v D) = f:B(x) _ :C(x) _ D(x); :G(x) _ D(x)g;
(B t D v E) = f:B(x) _ E(x); :D(x) _ E(x)g: For the above clauses, the bounded Herbrand universe consists of a single element: fag. Either this clause set has a model with domain fag or it does not have a model at all. Furthermore, for this particular clause set resolution is already 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 nd 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 di ers when it is lifted to DL axiom. The axiom B tD v E is relevant but its translation consists of only semi-relevant (but not relevant) clauses.
The notions relevant axioms and semi-relevant axioms are related to two problems in description logics: justi cations and repairs. Given an ontology O and an axiom s.t. O j= , a justi cation for O j= is a subset-minimal set J O s.t. J j= [10,20]. A generalisation of justi cations is the concept of a MinA [1], which denotes a minimal axiom set preserving some given property. The process of computing justi cations and MinAs is known as axiom pinpointing. Justi cations are classically used for explaining entailments observed by a reasoner, for which they are used for example in the ontology editor Protege [14]. Axioms that occur in at least one justi cation 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 correspond 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 justi cation.
If an axiom occurs in a justi cation for , in the translation into rst order logic, the axiom will be involved in some proof for O j= . Thus, every axiom in a justi cation 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 justi cation, as the following example shows. Example 9. Consider the ontology O = T [ A consisting of the TBox:
T = fA v B; B u C v D; B t D v Eg and the ABox A = fA(a); C(a)g; and consider the entailment O j= E(a). There is only one justi cation for this entailment, namely fA v B; B t D v E; A(a)g, 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 rst proof in rst-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 between axioms and entailments that are not captured by the classical notion of justi cation or MinA-relevance.
The notion of relevant axioms is also related to what has been studied in the eld of propositional satis ability under the name of lean kernels [11,12]: given an unsatis able 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 semirelevant 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 justi cation for O j= is a subset of M. There is no minimality requirement, that is, a MinApreserving module may contain axioms that do not occur in any justi cation. Because every axiom in a justi cation is also semi-relevant, the set of all semirelevant 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 rst-order clauses, there is also a connection to laconic justi cations [7]. A laconic justi cation departs from a justi cation 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 justi cation, 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 justi cations.
O = fA v B u C; D t B v Eg: The whole ontology is a justi cation for O j= A v E. However, the concepts C and D are super uous, i.e., they are not needed for the entailment, so that the axioms would be simpli ed for the laconic justi cation. The laconic justi cation is thus J = fA v B; B v Eg.
Now consider the rst-order translation of O.
:A(x) _ B(x); :A(x) _ C(x); :D(x) _ E(x); :B(x) _ E(x)
(
While axioms in justi cations correspond to semi-relevant axioms, an axiom that occurs in all justi cations corresponds to a relevant axiom. When exhibiting justi cations, it is helpful to understand whether they occur only in one justication or in several. This is for instance re ected in the visual presentation of justi cations in Protege [15], that indicates for each axiom in a justi cation in how many justi cations it is included, or whether it is included in every justi cation.
Another important connection however is from relevant axioms to repairs. In ontology repair, the aim is to remove an unwanted entailment from an ontology. Speci cally, a repair for an entailment O j= is a subset-minimal set R O s.t. O n R 6j= [8]. A repair for O j= always contains one axiom from every justi cation for O j= , 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 justi cations, our method provides a way of computing these repairs directly.
Two nal formalisms worth mentioning are provenance semirings and axiom pinpointing formulas, as they both are often used to link inferences to entailments. Given an entailment and an ontology O, a pinpointing formula is a monotone propositional formula over the axioms in O (as propositional symbols) s.t. every model of the formula entails , and the set of justi cations corresponds exactly to the set of minimal models of . Thus, pinpointing formulas can be used to generate justi cations, 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 E L in [2]. This idea of pinpointing formulas is very related to that of provenance semirings from the eld of database access [6], recently investigated also in the context of DLs [3]. Here the idea is to compute a formula, called provenance polynomial, that links a query result or entailment to the database entries that are involved in computing the query. 6
We introduced the notions of relevance and semi-relevance in rst-order logic, showed their e ectiveness and discussed their relationship to existing notions known in the DL context. Our notion of relevance adds new aspects in understanding an ontology to the related DL notions of justi cations and repairs. In particular, semi-relevant clauses appear to be particularly connected to laconic justi cations and the computation of relevant axioms o ers an alternative to existing repair methods.
The test procedure suggested in Section 4 relying on an explicit nite domain can be ine cient. It would be desirable to use the original rst-order decision procedures, 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 complete SOS procedure for ordered resolution. In any case, the design of an e cient 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".