Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The importance of Description Logics (DLs) cannot be overstated, and impact a growing number of fields. The \(\mathcal {EL}\)-family of tractable DLs in particular has been used to build large ontologies from the life sciences [34, 35]. Ontology development is an error-prone task, with potentially critical consequences in the life sciences; thus it is important to develop automated tools to help debugging large ontologies. Axiom pinpointing refers to the task of finding the precise axioms in an ontology that cause a (potentially unwanted) consequence to follow [25]. Recent years have witnessed remarkable improvements in axiom pinpointing technologies, including for the case of the \({\mathcal {EL}}\) family of DLs [1, 2, 5–7, 20, 21, 30, 31]. Among these, the use of SAT-based methods [1, 2, 30] was shown to outperform other alternative approaches very significantly. This is achieved by reducing the problem to a propositional Horn formula, which is then analyzed with a dedicated decision engine for Horn formulae.

This paper describes a tool, BEACON, that builds on recent work on efficient enumeration of Minimal Unsatisfiable Subsets (MUSes) of group Horn formulae, which finds immediate application in axiom pinpointing of \({\mathcal {EL}}\) ontologies [2]. In contrast to earlier work [2], which used EL+SAT [30, 31] as front-end, this paper proposes an integrated tool to perform analysis on ontologies, offering a number of new features.

The rest of the paper is organized as follows: Sect. 2 introduces some preliminaries. Section 3 describes the organization of BEACON. Experimental results are given in Sect. 4. Finally, Sect. 5 concludes the paper.

2 Preliminaries

2.1 The Lightweight Description Logic \(\mathcal {EL}^{+}\)

\(\mathcal {EL}^{+}\) [4] is a light-weight DL that has been successfully used to build large ontologies, most notably from the bio-medical domains. As with all DLs, the main elements in \(\mathcal {EL}^{+}\) are concepts. \(\mathcal {EL}^{+}\) concepts are built from two disjoint sets \(\mathsf {N}_{\mathsf {C}}\) and \(\mathsf {N}_{\mathsf {R}}\) of concept names and role names through the grammar rule \(C\, {:}{:}=\, A \mid \top \mid C\sqcap C \mid \exists r.C\), where \(A\in \mathsf {N}_{\mathsf {C}}\) and \(r\in \mathsf {N}_{\mathsf {R}}\). The knowledge of the domain is stored in a TBox (ontology), which is a finite set of general concept inclusions (GCIs) \(C\sqsubseteq D\), where C and D are \(\mathcal {EL}^{+}\) concepts, and role inclusions (RIs) \(r_1\circ \cdots \circ r_n\sqsubseteq s\), where \(n\ge 1\) and \(r_i,s\in \mathsf {N}_{\mathsf {R}}\). We will often use the term axiom to refer to both GCIs and RIs. As an example, Appendix \( \sqsubseteq \exists \) partOf.Intestine represents a GCI.

The semantics of this logic is based on interpretations, which are pairs of the form \(\mathcal {I}=(\varDelta ^{\mathcal {I}},\cdot ^{\mathcal {I}})\) where \(\varDelta ^{\mathcal {I}}\) is a non-empty set called the domain and \(\cdot ^{\mathcal {I}}\) is the interpretation function that maps every \(A\in \mathsf {N}_{\mathsf {C}}\) to a set \(A^{\mathcal {I}}\subseteq \varDelta ^{\mathcal {I}}\) and every \(r\in \mathsf {N}_{\mathsf {R}}\) to a binary relation \(r^{\mathcal {I}}\subseteq \varDelta ^{\mathcal {I}}\times \varDelta ^{\mathcal {I}}\). The interpretation \(\mathcal {I}\) satisfies the GCI \(C\sqsubseteq D\) iff \(C^{\mathcal {I}}\subseteq D^{\mathcal {I}}\); it satisfies the RI \(r_1\circ \cdots \circ r_n\sqsubseteq s\) iff \(r_1^{\mathcal {I}}\circ \cdots \circ r_n^{\mathcal {I}}\subseteq s^{\mathcal {I}}\), with \(\circ \) denoting composition of binary relations. \(\mathcal {I}\) is a model of \(\mathcal {T}\) iff \(\mathcal {I}\) satisfies all its GCIs and RIs.

The main reasoning problem in \(\mathcal {EL}^{+}\) is to decide subsumption between concepts. A concept C is subsumed by D w.r.t. \(\mathcal {T}\) (denoted \(C\sqsubseteq _{\mathcal {T}} D\)) if for every model \(\mathcal {I}\) of \(\mathcal {T}\) it holds that \(C^{\mathcal {I}}\subseteq D^{\mathcal {I}}\). Classification refers to the task of deciding all the subsumption relations between concept names appearing in \(\mathcal {T}\). Rather than merely deciding whether a subsumption relation follows from a TBox, we are interested in understanding the causes of this consequence, and repairing it if necessary.

Definition 1

(MinA, diagnosis). A MinA for \(C\sqsubseteq D\) w.r.t. the TBox \(\mathcal {T}\) is a minimal subset (w.r.t. set inclusion) \(\mathcal {M}\subseteq \mathcal {T}\) such that \(C\sqsubseteq _{\mathcal {M}} D\). A diagnosis for \(C\sqsubseteq D\) w.r.t. \(\mathcal {T}\) is a minimal subset (w.r.t. set inclusion) \(\mathcal {D}\subseteq \mathcal {T}\) such that \(C\not \sqsubseteq _{\mathcal {T}{\setminus }\mathcal {D}} D\).

MinAs and diagnoses are closely related by minimal hitting set duality [19, 29].

Example 2

Consider the TBox \({\mathcal {T}}_{\mathrm{{exa}}}=\{A\sqsubseteq \exists r.A, A\sqsubseteq Y, \exists r.Y\sqsubseteq B, Y\sqsubseteq B\}\). There are two MinAs for \(A\sqsubseteq B\) w.r.t. \({\mathcal {T}}_{\mathrm{{exa}}}\), namely \(\mathcal {M}_1=\{A\sqsubseteq Y, Y\sqsubseteq B\}\), and \(\mathcal {M}_2=\{A\sqsubseteq \exists r.A, A\sqsubseteq Y, \exists r.Y\sqsubseteq B\}\). The diagnoses for this subsumption relation are \(\{A\sqsubseteq Y\}\), \(\{A\sqsubseteq \exists r.A, Y\sqsubseteq B\}\), and \(\{\exists r.Y\sqsubseteq B, Y\sqsubseteq B\}\).

2.2 Propositional Satisfiability

We assume familiarity with propositional logic [9]. A CNF formula \({\mathcal {F}}\) is defined over a set of Boolean variables X as a finite conjunction of clauses, where a clause is a finite disjunction of literals and a literal is a variable or its negation. A truth assignment is a mapping \(\mu \): \(X \rightarrow \{ 0,1 \}\). If \(\mu \) satisfies \({\mathcal {F}}\), \(\mu \) is referred to as a model of \({\mathcal {F}}\). Horn formulae are those composed of clauses with at most one positive literal. Satisfiability of Horn formulae is decidable in polynomial time [12, 15, 24]. Given an unsatisfiable formula \({\mathcal {F}}\), the following subsets are of interest [19, 22]:

Definition 3

(MUS, MCS). \({\mathcal {M}}\subseteq {\mathcal {F}}\) is a Minimally Unsatisfiable Subset (MUS) of \({\mathcal {F}}\) iff \({\mathcal {M}}\) is unsatisfiable and \(\forall {c\in {\mathcal {M}}}, {\mathcal {M}}\setminus \{ c \}\) is satisfiable. \({\mathcal {C}}\subseteq {\mathcal {F}}\) is a Minimal Correction Subset (MCS) iff \({\mathcal {F}} \setminus {\mathcal {C}}\) is satisfiable and \(\forall {c\in {\mathcal {C}}}, {\mathcal {F}} \setminus ({\mathcal {C}}\setminus \{ c \})\) is unsatisfiable.

MUSes and MCSes are related by hitting set duality [8, 10, 28, 33]. Besides, these concepts have been extended to formulae where clauses are partitioned into groups [19].

Fig. 1.
figure 1

BEACON organization

Full size image

Definition 4

(Group-MUS). Given an explicitly partitioned unsatisfiable CNF formula \({\mathcal {F}} = {\mathcal {G}}_0 \cup ... \cup {\mathcal {G}}_k\), a group-MUS of \({\mathcal {F}}\) is a set of groups \( {\mathcal {G}} \subseteq \{ {\mathcal {G}}_1, ... , {\mathcal {G}}_k \}\), such that \({\mathcal {G}}_0 \cup {\mathcal {G}}\) is unsatisfiable, and for every \({\mathcal {G}}_i \in {\mathcal {G}}\), \({\mathcal {G}}_0 \cup ({\mathcal {G}} \setminus {\mathcal {G}}_i)\) is satisfiable.

3 The BEACON Tool

The main problem BEACON is aimed at is the enumeration of the MinAs and diagnoses for a given subsumption relation w.r.t. an \(\mathcal {EL}^{+}\) TBox \(\mathcal {T}\). BEACON consists of three main components: The first one classifies \(\mathcal {T}\) and encodes this process into a set of Horn clauses. Given a subsumption to be analyzed, the second component creates and simplifies an unsatisfiable group Horn formula. Finally, the third one computes group-MUSes and group-MCSes, corresponding to MinAs and diagnoses resp. Figure 1 depicts the main organization of BEACON. Each of its components is explained below.

3.1 Classification and Horn Encoding

During the classification of \(\mathcal {T}\), a Horn formula \({\mathcal {H}}\) is created according to the method introduced in EL\(^{ + }\)SAT  [30, 31]. To this end, each axiom \(a_i \in \mathcal {T}\) is initially assigned a unique selector variable \(s_{[a_i]}\). The classification of \(\mathcal {T}\) is done in two phases [4, 6].

First, \(\mathcal {T}\) is normalized so that each of its axioms are of the form (i) \((A_1 \sqcap ... \sqcap A_k) \sqsubseteq B\) (\(k \ge 1\)), (ii) \(A \sqsubseteq \exists r.B\), (iii) \(\exists r.A \sqsubseteq B\), or (iv) \(r_1 \circ ... \circ r_n \sqsubseteq s\) (\(n \ge 1\)), where \(A, A_i, B \in \mathsf {N}_{\mathsf {C}}\) and \(r, r_i, s \in \mathsf {N}_{\mathsf {R}}\). This process results in a TBox \(\mathcal {T}_{{\mathcal {N}}}\) where each axiom \(a_i \in \mathcal {T}\) is substituted by a set of axioms in normal form \(\{a_{i1}, ..., a_{im_i}\}\). At this point, the clauses \(s_{[a_i]} \rightarrow s_{[a_{ik}]}\), with \(1 \le k \le m_i\), are added to \({\mathcal {H}}\).

Second, \(\mathcal {T}_{{\mathcal {N}}}\) is saturated through the exhaustive application of the completion rules shown in Table 1, resulting in the extended TBox \(\mathcal {T}'\). Each of the rows in Table 1 constitute a completion rule. Their application is sound and complete for inferring subsumptions [4]. Whenever a rule r can be applied (with antecedents \(\mathsf {ant}(r)\)) leading to inferring an axiom \(a_i\), the Horn clause \((\bigwedge _{\{a_j\in \mathsf {ant}(r)\}} s_{[a_j]})\rightarrow s_{[a_i]}\) is added to \({\mathcal {H}}\).

As a result, \({\mathcal {H}}\) will eventually encode all possible derivations of completion rules inferring any axiom such that \(X \sqsubseteq _{{\mathcal {T}}} Y\), with \(X, Y \in \mathsf {N}_{\mathsf {C}}\).

Table 1. \(\mathcal {EL}^{+}\) completion rules
Full size table

3.2 Generation of Group Horn Formulae

After classifying \(\mathcal {T}\), some axioms \(C \sqsubseteq D\) may be included in \(\mathcal {T}'\) for which a justification or diagnosis may be required. Each of these queries will result in a group Horn formula defined as: \({\mathcal {H}}_G = \{{\mathcal {G}}_0, {\mathcal {G}}_1, ..., {\mathcal {G}}_{|\mathcal {T}|}\}\), where \({\mathcal {G}}_0 = {\mathcal {H}} \cup \{(\lnot s_{[C\sqsubseteq D]})\}\) and for each axiom \(a_i\) (\(i > 0\)) in the original TBox \(\mathcal {T}\), group \({\mathcal {G}}_i = \{(s_{[a_i]})\}\) is defined with a single unit clause. \({\mathcal {H}}_G\) is unsatisfiable and, as shown in [1, 2], its group-MUSes correspond to the MinAs for \(C \sqsubseteq _{{\mathcal {T}}} D\). Equivalently, due to the hitting set duality for MinAs/diagnoses, which also holds for MUSes/MCSes, group-MCSes of \({\mathcal {H}}_G\) correspond to diagnoses for \(C \sqsubseteq _{{\mathcal {T}}} D\).

BEACON simplifies \({\mathcal {H}}_G\) with the techniques introduced in [30, 31], which often reduce the formulas to a great extent.

3.3 Computation of Group-MUSes/Group-MCSes

For enumerating group-MUSes and group-MCSes of the formula \({\mathcal {H}}_G\) defined above, BEACON integrates the state-of-the-art HgMUS enumerator [2]. HgMUS exploits hitting set dualization between (group) MCSes and (group) MUSes and, hence, it shares ideas also explored in MaxHS [11], EMUS/MARCO [17, 26], among others. As shown in Algorithm 1, these methods rely on a two (SAT) solvers approach. Formula \({\mathcal {Q}}\) is defined over a set of selector variables corresponding to clauses in \({\mathcal {F}}\), and it is used to enumerate subsets of \({\mathcal {F}}\). Iteratively, the algorithm computes a maximal model P of \({\mathcal {Q}}\) and tests whether the subformula \( {\mathcal {F}}' \subseteq {\mathcal {F}}\) containing the clauses associated to P is satisfiable. If it is, \({\mathcal {F}} \setminus {\mathcal {F}}'\) is an MCS of \({\mathcal {F}}\). Otherwise, \({\mathcal {F}}'\) is reduced to an MUS. MCSes and MUSes are blocked adding clauses to \({\mathcal {Q}}\).

HgMUS shares the main organization of Algorithm 1, with \({\mathcal {F}} = {\mathcal {G}}_0\) and \({\mathcal {Q}}\) defined over selector variables for groups \({\mathcal {G}}_i\) of \({\mathcal {H}}_G\), with \(i > 0\). It also includes some specific features. First, it uses the Horn satisfiability algorithhm LTUR [24]. Besides, it integrates a dedicated insertion-based MUS extractor as well as an efficient algorithm for computing maximal models based on a reduction to computing MCSes [23].

figure a

3.4 BEACON’s Additional Specific Features

Besides computing MinAs/diagnoses, BEACON offers additional functionalities.

Diagnosing Multiple Subsumption Relations at a Time. After classifying \(\mathcal {T}\), there could be several unintended subsumption relations \(C_i \sqsubseteq _{{\mathcal {T}}} D_i\) that need to be removed. BEACON allows for diagnosing this multiple unintended inferences at the same time. By adding the unit clauses (\(\lnot s_{[C_i\sqsubseteq D_i]}\)) to \({\mathcal {G}}_0\) in \({\mathcal {H}}_G\), each computed group-MCS corresponds to a diagnosis that would eliminate all the indicated subsumption relations.

Computing Smallest MinAs. Alternatively to enumerating all the possible MinAs, one may want to compute only those of the minimum possible size. To enable this functionality, BEACON integrates a state-of-the-art solver for the smallest MUS problem (SMUS) called Forqes [14]. The decision version of the SMUS problem is known to be \(\varSigma _2^{ P }\)-complete (e.g. see [13, 16]). As HgMUS, Forqes is based on the hitting set dualization between (group) MUSes and (group) MCSes. The tool iteratively computes minimum hitting sets of a set of MCSes of a formula detected so far. While these minimum hitting sets are satisfiable, they are grown into an MSS, whose complement is an MCS which is added to the set of MCSes. The process terminates when an unsatisfiable minimum hitting set is identified, representing a smallest MUS of the formula.

4 Experimental Results

This section reports a summary of results that illustrates the performance of BEACONFootnote 1 w.r.t. other \(\mathcal {EL}^{+}\) axiom pinpointing tools in the literature. It also provides information on its capability of computing diagnoses and enumerating smallest MinAs.

The experiments were run on a Linux cluster (2 Ghz) with a limit of 3600 s and 4Gbyte, considering 500 subsumption relations from five well-known \(\mathcal {EL}^{+}\) bio-medical ontologies: GALEN [27] (FULL-GALEN and NOT-GALEN), Gene [3], NCI [32] and SNOMED-CT [34]. The experiments use Horn formulae encoded by EL\(^{ + }\)SAT  [30, 31] applying the reduction techniques that BEACON incorporates by default. These formulae are fed to BEACON’s engines, namely HgMUS and Forqes.

The results reported focus on HgMUS and Forqes. Due to lack of space, running times for classifying the ontologies and formula reduction are not reported. Classification is done in polynomial time once for each ontology, so it is amortized among all queries for the ontology. Formula reduction usually takes very short time. Detailed results are available with the distribution of BEACON, including an analysis on the size of the Horn formulae and the reductions achieved.

Fig. 2.
figure 2

Plots comparing BEACON to EL\(^{ + }\)SAT, SATPin and JUST

Full size image

Axiom Pinpointing. BEACON shows significant improvements over the existing tools EL\(^{ + }\)SAT  [30, 31], SATPin [21], EL2MCS [1], CEL [5] and Just  [20]. BEACON often achieves remarkable reductions in the running times, and exhibits a clear superiority in enumerating MinAs for 19 very hard instances that cannot be solved by a time limit of 3600 s. This is illustrated in Fig. 2. The cactus plot shows the number of MinAs reported over time. BEACON computes much more MinAs faster than other tools. The scatter plot compares BEACON with Just regarding the running times on a subset of the instances Just can cope with. BEACON shows a significant performance gap. Similar results have been observed for EL2MCS and CEL [2].

Computing Diagnoses. For all solved instances (481 out of 500), BEACON enumerates all diagnoses, where its number ranges from 2 to 565409. Interestingly, for the 19 aborted instances, the number of reported diagnoses ranges from 1011164 to 1972324. These numbers illustrate the efficiency of BEACON at computing diagnoses, and explain the difficulty of these aborted instances. Of the other tools, only EL2MCS reports diagnoses, which, for hard instances, computes around 33 % fewer diagnoses.

Computing Smallest MinAs. The last experiments consider the 19 instances for which BEACON is unable to enumerate all MinAs. Notably, BEACON is very efficient at computing the smallest MinAs using \(\textsc {Forqes}\). In all cases, each set of smallest MinAs is computed in negligible time (less than 0.1 s). The sizes of the smallest MinAs range from 5 to 13 axioms, and their number ranges from 1 to 7.

5 Conclusions

This paper describes BEACON, an axiom pinpointing tool for the \(\mathcal {EL}\)-family of DLs. BEACON integrates HgMUS  [2], a group MUS enumerator for propositional Horn formulae, with a dedicated front-end, interfacing a target ontology, and generating group Horn formulae for HgMUS. Besides enumerating MinAs (and associated diagnoses), BEACON enables the simultaneous diagnosis of multiple inferences, and the computation of the smallest MinA (or smallest MUS [14]). The experimental results indicate that the computation of the smallest MinA is very efficient in practice, in addition to the already known top performance of HgMUS.