Axiom pinpointing is the task of identifying the axiomatic causes for a consequence to follow from an ontology. Diferent approaches have been proposed in the literature for finding one or all justifications: the subset-minimal subontologies that preserve a description logic consequence. We propose an approach that leverages the capabilities of answer set programming-through minimal unsatisfiable subset enumeration-for transparent axiom pinpointing. Our approach is general in that it allows one to seamlessly specify the ontology and the reasoning rules, thus being applicable to diferent logics without modification to the core method. We showcase this generality by introducing methods for ℰℒ and for Horn-ℒ, and explaining how to apply it to other logics. A preliminary experiment shows the practicality of the approach.
Axiom pinpointing [
To-date, the most successful approach to axiom pinpointing which does not rely on repeated
(black-box) calls to a standard reasoner is a reduction to the enumeration of the minimal
unsatisfiable subsets (MUS) of clauses of a propositional formula [
The main disadvantage of these approaches is that they require, as a pre-processing step,
the construction of a huge propositional formula, which makes the reasoning steps explicit. In
other words, the encoding step requires an implementation of the ℰℒ completion algorithm
(or a consequence-based algorithm) with a modification to generate the propositional clauses.
This in particular means that the approach cannot be easily adapted to diferent logics, as new
implementations of the full decision procedure would be necessary. On the other hand, they
have the advantage that any MUS enumerator can be applied on the derived formula, thus
leveraging the fast developments from SAT [
Our goal is to keep the advantages of the reduction to MUS enumeration, while at the same
time allowing a higher flexibility to handle diferent kinds of languages, and in particular,
diferent DLs beyond ℰℒ. We thus propose a new approach to axiom pinpointing based on a
translation to Answer Set Programming (ASP) [
As an example of its applicability, we instantiate our approach to deal with axiom pinpointing in Horn-ℒ and its sublogic ℰℒ. We also explain the changes to handle the very inexpressive ℋℒ, which essentially corresponds to hypergraph reachability. We also implemented a tool called OWL2ASP, which translates (for now) ℰℒ ontologies to our ASP format, and calls a variant of the ASP solver WASP to enumerate the MUSes and thus the justifications. We present a first preliminary analysis of its performance on realistic ontologies.
The seed ideas of this paper were originally presented in [
We start by briefly introducing the notions of answer set programming, DLs, and axiom pinpointing that are needed for understanding our approach.
Answer set programming (ASP) [
In ASP, a variable is a string starting with uppercase letter; a constant is an integer or a
string starting with lowercase letter; and an atom is an expression of the form (1, . . . , )
where is a predicate of arity and 1, . . . , are terms. An atom is ground if it contains no
variables. A literal is a atom or its negation where denotes negation as failure. A
literal ℓ is negative if it is of the form , otherwise it is positive. The complement of positive
(resp. negative) literal ℓ = (resp. ℓ = ), denoted by ℓ, is the literal (resp. ). A
(normal) rule is an expression of the form ℎ ← 1, . . . , where 1, . . . , is a conjunction of
literals, called the body, ≥ 0, and ℎ is an atom called the head. All variables in a rule must
occur in some positive literal of the body (i.e., are safe cf. [
Given a program , the Herbrand Universe denotes the set of constants in ; the Herbrand
Base denotes the set of standard ground atoms that can be obtained from predicate in and
constants in . Given a rule ∈ , () denotes the set of possible rule instantiations
that can be obtained by replacing variables in with constants in . The ground instantiation
of the program , denoted by ( ), is the union of ground instantiations of rules in
. An interpretation is a subset of . Given an interpretation , a positive (resp. negative)
literal ℓ is true w.r.t. , if ℓ ∈ (resp. ℓ ∈/ ); it is false if ℓ ∈/ (resp. ℓ ∈ ). A conjunction of
literals is true w.r.t. if all the literals are true w.r.t. . An interpretation is a model of if for
each ∈ ( ), the head of is true whenever the body of is true. The choice rule {}
simply guesses whether is made true or not. Given a program and an interpretation , the
(Gelfond-Lifschitz) reduct [
In the following sections, all ASP symbols are often denoted with a typewriter font, to distinguish them from other mathematical symbols, and rules use :- instead of ← .
We assume familiarity with description logics (DLs) [
Starting from two infinite, disjoint sets and or concept names and role names, respectively, ℒ-concepts are constructed through the grammar rule
::= | ⊤ | ⊥ | ¬ | ⊓ | ⊔ | ∃. | ∀., where ∈ and ∈ . A GCI is an expression of the form ⊑ where and are concepts. A TBox is a finite set of GCIs.
To define Horn- ℒ we need the notion of polarity for each occurrence of a concept in an expression, which is defined recursively as follows. Each concept occurs positively in ; if occurs positively (resp. negatively) in ′, then (i) it also occurs positively (resp. negatively) in ′ ⊓ , ′ ⊔ , ∃.′, ∀.′ and ⊑ ′ (considering commutativity of ⊓, ⊔) and (ii) it occurs negatively (resp. positively) in ¬′ and ′ ⊑ . Horn-ℒ is the sublogic of ℒ in which axioms with positive occurrences of ⊔ or negative occurrences of ¬ or ∀. are disallowed. ℰℒ is another sublogic of ℒ, where the constructors ¬, ⊔, ∀, and ⊥ are not allowed. In particular, ℰℒ is also a fragment of Horn-ℒ. As an additional example, we consider also the fragment ℋℒ (also known as ℒ0) of ℰℒ in which only concept names and conjunctions (⊓) are allowed.
The semantics of ℒ (and its fragments) is defined through interpretations, which are pairs ℐ = (∆ ℐ , · ℐ ) with ∆ ℐ a non-empty set called domain and · ℐ is the interpretation function mapping every ∈ to a set ℐ ⊆ ∆ ℐ and every ∈ to a binary relation ℐ ⊆ ∆ ℐ × ∆ ℐ . The interpretation function is extended to concepts setting ⊤ℐ := ∆ ℐ , (¬)ℐ := ∆ ℐ ∖ ℐ , ( ⊓ )ℐ := ℐ ∩ ℐ , and (∃.)ℐ := { | ∃ ∈ ℐ .(, ) ∈ ℐ }. The other constructors are treated analogously. The interpretation ℐ satisfies the GCI ⊑ if ℐ ⊆ ℐ . It is a model of if it satisfies all GCIs in . We often call GCIs axioms, which allows us to seamlessly connect between DL and arbitrary representation languages. The TBox entails the GCI ⊑ ( |= ⊑ ) if every model of satisfies ⊑ . In this case we say that ⊑ is a consequence of .
We focus on the problem of deciding atomic subsumption relations ⊑ where , ∈ .
The consequence-based algorithm for Horn-ℒ [
In the case of ℰℒ, the last kind of normal form axiom will never appear, and the concept appearing in the right-hand side of the first two kinds can never be ⊥. Hence, the first four rules in Table 1 sufice for atomic subsumption in this logic. For practical reasons, in this case we will unify two rules into one with a larger set of preconditions, which will sufice for deciding atomic subsumptions. It can be seen that ℋℒ is a syntactic variant of directed hypergraphs. Specifically, a GCI 1 ⊓ · · · ⊓ ⊑ 1 ⊓ · · · ⊓ represents a directed hypergraph connecting nodes 1, . . . , with nodes 1, . . . , , and the entailment problem is nothing more than reachability in this hypergraph.
Beyond standard reasoning, it is sometimes important to understand which axioms are responsible for a consequence to follow from a TBox. This goal is often instantiated as the task of identifying justifications .
Definition 1. A justification for a consequence w.r.t. the TBox is a set ℳ ⊆ ℳ |= and (ii) for every ⊂ ℳ , ̸|= . such that (i)
Briefly, a justification is a subset-minimal sub-TBox that still entails the consequence.
Importantly, justifications refer to the GCIs in the original TBox before normalisation, which means
an additional minimisation step if the pinpointing method works on normalised TBoxes [
Most work focuses on computing one or all justifications. While the former problem remains
polynomial in ℰℒ, the latter necessarily needs exponential time, as the number of justifications
may be exponential on the size of the TBox. Despite some potential uses, which have been
identified for non standard reasoning [
A similar problem is observed in ASP. When a program is incoherent, one may want to find
the minimal sub-programs that are still incoherent. This notion, analogous to justifications in
DLs, is called a minimal unsatisfiable subset (MUS) in the ASP community [
Before presenting our approach to axiom pinpointing using ASP, we briefly describe how to reduce reasoning in Horn-ℒ to ASP. The approach simulates the completion algorithm sketched in Section 2.2 through a small set of rules, while the TBox axioms (in normal form) are represented through facts.
Consider a TBox in normal form, and let ( ) and ℛ( ) be the sets of concept names and role names appearing in , respectively. For each ∈ ( ) we use a constant a, and for each ∈ ℛ( ) we use a constant r. We also use the numerical constants 0 and 1 for ⊥ and ⊤, respectively. We identify the four shapes of normal form axioms via a diferent predicate s0, . . . , s4 as shown in Figure 1 (left). Hence, s0(a,b) stands for the GCI ⊑ and so on. For each axiom in normal form appearing in , we write the associated fact. As previously mentioned, the reasoning process is simulated through rules. In the specific case of Horn- ℒ, these rules are shown in the right-hand side of Figure 1. As before, if the TBox belongs to ℰℒ, then the first four rules sufice (and the last two can be removed from the program). For eficiency reasons, in the ℰℒ encoding we merge the third and fourth rules into one. To decide whether the atomic subsumption ⊑ is a consequence of the TBox, we need only ask the query s0(a,b); i.e., check whether this fact is derivable from the initial facts, applying the rules. Since the original TBox may not be in normal form, the facts obtained this way are the result of
ASP fact ⊑ s0(a,c). 1 ⊓ 2 ⊑ s1(a1,a2,c). ⊑ ∃. s2(a,r,b). ∃. ⊑ s3(r,a,b). ⊑ ∀. s4(a,r,b).
s0(X,Y) :- s0(X,Z), s0(Z,Y). s0(X,Y) :- s0(X,Z1), s0(X,Z2), s1(Z1,Z2,Y). s2(X,R,Y) :- s2(X,R,Z), s0(Z,Y). s0(X,Y) :- s2(X,R,Z), s3(R,Z,Y). s2(X,R,Y) :- s2(X,R,Z1), s4(X,R,Z2), s1(Z1,Z2,Y).
s0(X,0) :- s2(X,R,Y), s0(Y,0). the normalisation step over the original GCIs. As we will see later, we can use additional rules to preserve the origin information for each normalised GCI, which will be useful for axiom pinpointing.
In the case of ℋℒ, one can produce a more direct reduction, which takes into account
the hyperedges without the need for normalisation or general derivation rules. We again
represent each concept name through a constant a, and associate a new constant gi for
each GCI in . Then the GCI 1 ⊓ · · · ⊓ ⊑ 1 ⊓ · · · ⊓ is translated to the set of
rules {gi :- a1, . . . , am., b1 :- gi., . . . , bn :- gi.}. To decide whether ⊑ is a
consequence, we add the fact a. and verify the query b. The correctness of these approaches
follows from the results in [
We present a general approach for solving axiom pinpointing tasks through an ASP solver. The approach is applicable to any logic (including other DLs) which allows for a modular ASP encoding. Roughly, an encoding is a function that maps TBoxes (or more generally, knowledge bases) to ASP programs, and it is modular if each axiom in translates to a set of rules, such that an ASP encoding Π of is obtained by the union of the encodings of its axioms, possibly together with some additional rules (independent of the specific axioms in ) needed to simulate reasoning in ASP.
Definition 2. An encoding in ASP Π is modular if for every TBox it holds that (i) for each ∈ there is an ASP program Π , and (ii) there is a (possibly empty) set of rules such that Π = ⋃︀ ∈ Π ∪
The encodings from Section 3 for Horn-ℒ, ℰℒ and ℋℒ are all modular. In the first two cases, is the set of rules in Figure 1 (right), while in the latter = ∅. For any (arbitrary) Horn-ℒ GCI , Π is the ASP representation of its translation to normal form. We now formulate the problem of computing all justifications in ASP. First, we apply an adornment step, which allows to identify and keep track of the rules of a module corresponding to a given axiom, necessary for pinpointing.
Definition 3. Let be an ASP program, and be an atom not occurring in . The -adornment for is the program ∆ ( ) = { | ∈ }, where is such that ℎ( ) = ℎ(), and ( ) = () ∪ .
In words, the -adornment adds a new identifying atom to the body of each rule of the program. This guarantees that the rules trigger only when is true. In the case of Horn-ℒ, which means that axioms in normal form will be considered only if the original axiom that produces them is considered.
Definition 4. The adorned ASP encoding of the TBox is the program (Π ) = ⋃︁ ∆ (Π ) ∪ ∪
∈ containing a choice rule { } for each ∈ . where for each
∈ , is a fresh atom not occurring in Π( ), and is the ASP program
In the case of Horn-ℒ and ℰℒ, the adornment will change each fact (corresponding to a
GCI in normal form) si(_). into the rule si(_) :- xj, where xj is the chosen constant for
the original (DL) axiom . Importantly, this approach handles the original axioms in the TBox,
and not those already normalised as done e.g. in [
We now describe an ASP program that can be used for axiom pinpointing. Note that ⊑ is a consequence of if and only if the program (Π ) entails the atom s0(a,b). Thus, incoherence. In other words, the MUSes. if we add the constraint :-s0(a,b). the resulting program will be incoherent. To find out the justifications for ⊑ (the minimal subset of axioms that entail it), it sufices to find the minimal subsets of adornments—which refer to the original axioms in —that preserve ∈ ℳ} = ∩ { |
∈ }. = (Π ) ∪ {← such that { | Proposition 1. Let be a TBox, an atom modelling a consequence of , and the program }. ℳ ⊆ is a justification for if there is a MUS of w.r.t. { | ∈ }
Justifications that are cardinality minimal (and thus also subset minimal) can be directly computed using an ASP program with weak constraints. In a nutshell, a weak constraint :∼a tries to exclude the atom a from any model, but can be introduced if necessary. In this case, the MUS enumerator tries to minimise the number of weak constraints that are violated which corresponds to minimising the cardinality of the associated justification.
Proposition 2. Let be a TBox, an atom modelling a consequence of , and the program = (Π ) ∪ {← } ∪ {:∼ |
∈ }. ℳ ⊆ there exists an optimal MUS of such that { | ∈ ℳ} = ∩ { |
∈ }. is a cardinality-minimal justification for if
Before describing our implementation and empirical evaluation, we note that the translation
permits computing the intersection of all justifications, and consequences derived from it,
through the application of cautious reasoning [
The translator takes an ℰℒ TBox and produces five files which include all the information about the original axioms, the normalised GCIs they produce, and a mapping from concept and role names (in DL) and constants (in ASP). As it is standard, we use integers as ASP constants to reduce the consumption of memory and other resources. Specifically, for a given TBox , OWL2ASP generates (i) a file asp.txt which contains the ASP translation of the normalisation of together with the information of which original axioms produced them using a new predicate symbol o(_) to better capture the origin; (ii) originalAxioms.txt containing an (integer) ID for each OWL-represented axiom in the original ontology; (iii) owlElements.txt relating the concept and role names with unique integer IDs; (iv) axiom_facts.asp enumerating the IDs of original axioms for aiding the ASP MUS enumerator; and (v) encoding.asp enumerating the reasoning rules and the query of interest.
Note that in the current implementation, the file encoding.asp is the same for any possible input TBox modulo the requested query: it always contains the first four rules shown in Figure 1 (right).2 Yet, here lies the flexibility in our approach: to handle other formalisms, one needs only to change this file with the corresponding rules, and—perhaps the largest efort—implement the normalisation procedure for the new language. The rest of the approach remains unchanged, which means that ASP features can be used without issues.
The resulting files can be fed to an ASP solver to verify that the consequence expressed in
the query follows from the TBox. But our goal is rather to enumerate the justifications for
this consequence. Thus, the tool adds a choice rule for each atom representing an original
GCI from , and calls the MUS enumerator of WASP3 [
We executed a preliminary experiment to empirically assess the potential of our method. For this experiment we consider the well-known biomedical ontology NOT-GALEN, which is among the de facto benchmarks for axiom pinpointing in ℰℒ. More precisely, we consider the version provided in jcel,4 which features 4379 axioms, 2748 concepts, and 413 roles, and chose a random sample of 25 queries on this ontology already considered in the literature. The task we consider is the enumeration of all justifications for each query.
Our tool, called OWL2ASP, employs the encoding from Figure 1 targeted for ℰℒ, with the
third and fourth rules combined into one. The resulting program was first processed through
the magic sets technique [
We compare with other glass-box axiom pinpointing tools for ℰℒ. In particular, we run three
methods based on a translation to SAT originally proposed by Sebastiani and Vescovi—namely
EL2SAT [
The results of the execution are reported in Table 2, which shows the solving time in seconds for each query and tool. For the cells denoted by < 0.01, the execution time was below the sampling range of the observation wrapper we used. For our tool (OWL2ASP) we report the time needed by WASP to perform MUS enumeration without considering the pre-processing time to obtain propositional programs. This is to create a fair comparison with the SAT-based tools whose input is already a SAT formula encoding the full standard reasoning process. On the one hand, we report that OWL2ASP requires 0.8s on average (with a standard deviation of 0.15) to pre-process the input over all the 25 queries compared, which is a positive result. On the other hand, we observe that the experiment highlights the viability of the proposed approach; indeed, OWL2ASP results to be the fastest in terms of solving time for this sample, providing answers almost instantaneously.
We presented a general approach for axiom pinpointing based on a reduction to ASP. Similar
to existing SAT-based approaches, we construct an ASP program which, if extended with a
constraint encoding a consequence of interest, becomes incoherent; that is, has no models. Then,
an ASP MUS enumerator is used to find justifications eficiently. Importantly, even though the
reasoning step requires normalisation, our approach enumerates directly on the original axioms
in the TBox, thus avoiding an additional (potentially expensive) recovery step [
As a proof of concept, we have shown how the reduction works for the DL Horn-ℒ, and
its sublogics ℰℒ and ℋℒ. The same idea is applicable for any logic with a modular translation
to ASP, for instance any DL with a consequence-based reasoning algorithm [
EL2SAT OWL2ASP
1.not.galen
2.not.galen
3.not.galen
4.not.galen
5.not.galen
6.not.galen
7.not.galen
8.not.galen
9.not.galen
10.not.galen
11.not.galen
12.not.galen
13.not.galen
14.not.galen
15.not.galen
16.not.galen
17.not.galen
18.not.galen
19.not.galen
20.not.galen
21.not.galen
22.not.galen
23.not.galen
24.not.galen
25.not.galen
enjoy such a translation. The challenge in these cases is to find an adequate expression of the
consequence-based rules which can be handled by the ASP solver. For instance, the
consequencebased method for (full) ℒ manipulates sets, which are not native to ASP. Dealing with further
constructors imposes additional challenges. On the other hand, once such an encoding has been
devised, our approach can be seamlessly applied, without further implementation issues. In
contrast, existing methods based on SAT [
To test the applicability of our method, we implemented OWL2ASP, a tool that produces the corresponding encoding for ℰℒ TBoxes, and compare it with other glass-box methods for pinpointing in this logic. Our results are very promising, they show that our tool is competitive with state-of-the-art alternatives in a preliminary experiment considering 25 queries executed on NOT-GALEN. For future work, we plan to extend the evaluation to a larger sample of queries and ontologies, following existing benchmarks. We will also extend the implementation to handle Horn-ℒ.
An advantage of using an of-the-shelf ASP solver is that we can directly take advantage of all the services that these solvers provide without any additional cost. In particular, through a simple modification to the MUS enumerator call, one can obtain justifications of minimal cardinality. In the future, we plan to study the implementation of other axiom pinpointing services based on ASP constructs and evaluate their practical applicability. Moreover, we plan to further reduce the (already acceptable) pre-processing times by exploiting the modularity properties of the ontology in input, in order to specialise the reasoning task only to those modules that are involved in the input query.
This work was partially supported by MUR for the Department of Excellence DISCo at the University of Milano-Bicocca and under PRIN project PINPOINT Prot. 2020FNEB27, CUP H23C22000280006 and H45E21000210001. We would like to thank Carmine Dodaro for his support using the MUS enumerator.