Abstract

In this paper, we explore the issue of inconsistency handling over prioritized knowledge bases (KBs), which consist of an ontology, a set of facts, and a priority relation between conflicting facts. In the database setting, a closely related scenario has been studied and led to the definition of three different notions of optimal repairs (global, Pareto, and completion) of a prioritized inconsistent database. After transferring the notions of globally-, Pareto- and completion-optimal repairs to our setting, we study the data complexity of the core reasoning tasks: query entailment under inconsistency-tolerant semantics based upon optimal repairs, existence of a unique optimal repair, and enumeration of all optimal repairs. Our results provide a nearly complete picture of the data complexity of these tasks for ontologies formulated in common DL-Lite dialects. The second contribution of our work is to clarify the relationship between optimal repairs and different notions of extensions for (set-based) argumentation frameworks. Among our results, we show that Pareto-optimal repairs correspond precisely to stable extensions (and often also to preferred extensions), and we propose a novel semantics for prioritized KBs which is inspired by grounded extensions and enjoys favourable computational properties. Our study also yields some results of independent interest concerning preference-based argumentation frameworks.

1 Introduction↩︎

Ontology-mediated query answering (OMQA) improves data access through the use of an ontology, which provides a convenient vocabulary for query formulation and captures domain knowledge that is exploited during query evaluation [1]–[3]. There is now a large literature on OMQA, with much of the work adopting description logics (DLs) [4], or the closely related OWL (2) standard [5], as the ontology specification language. In particular, the DL-Lite family of lightweight DLs [6], [7] (which underpin the OWL 2 QL profile [8]) has been a main focus of both theoretical and practical research due to its favourable computational properties.

While it is often reasonable to assume that the ontology has been debugged and contains only trusted knowledge, real-world datasets are plagued by data quality issues, which may render the KB inconsistent. This has led to a large body of work on how to handle data inconsistencies in OMQA, with the proposal of several inconsistency-tolerant semantics to provide meaningful answers to queries posed over inconsistent KBs (see e.g.the surveys [9] and [10]). Many of these semantics are based upon some notion of repair, defined as an inclusion-maximal subset of the data that is consistent with the ontology. This is in particular the case for the AR, brave, and IAR semantics, which correspond respectively to a query answer holding w.r.t. all repairs, at least one repair, or the intersection of all repairs [11], [12]. The computational properties of these and other semantics are now quite well understood, and some practical algorithms and implementations have begun to be developed, see e.g.[13]–[16].

In many scenarios, there is some information about the dataset that can be used to select the most relevant repairs (e.g.we might know which relations or sources are most reliable, or the likelihood of certain kinds of facts being correct). To exploit such information, variants of the preceding semantics have been considered in which we restrict attention to the most preferred repairs based upon cardinality, weight, or a stratification of the dataset into priority levels [17]. While the latter forms of preferences are quite natural, there are other relevant ways of defining preferred repairs that are worth exploring. In particular, in the database area, the seminal work of [18] supposes that preferences are given in terms of a priority relation (i.e. acyclic binary relation) between conflicting facts. Such ‘fact-level’ preferences have been shown to naturally arise in applications like information extraction and can e.g.be declaratively specified using rules [19]. To lift a priority relation between facts to the level of repairs, three different methods were proposed by Staworko et al. Pareto-optimal and globally-optimal repairs are defined as those for which there is no possible substitution of facts that leads to a (Pareto / global) improvement, while completion-optimal repairs correspond to greedily constructing a repair based upon some compatible total order (see Section 3 for formal definitions). The complexity of reasoning with these three kinds of optimal repair has been investigated, primarily focusing on constraints given as functionality dependencies [20]–[22].

In this paper, we explore the use of fact-level preferences and optimal repairs for inconsistency handling in OMQA. Our first contribution is a data complexity analysis of the central reasoning problems related to optimal repairs: conjunctive query entailment under inconsistency-tolerant semantics based upon optimal repairs, uniqueness of optimal repairs, and enumeration of all optimal repairs. Our results provide a nearly complete picture of the data complexity for the three types of optimal repair and for ontologies formulated in DL-Lite\(_{\mathsf{core}}\) and DL-Lite\(^{\mathcal{H}}_\mathsf{horn}\); however, as we make precise later, many of our results transfer to other data-tractable ontology languages. Not surprisingly, we find that reasoning with optimal repairs is generally more challenging than for standard repairs. In particular, query entailment under variants of the AR, IAR, and brave semantics based upon any of the three notions of optimal repair is intractable in data complexity, whereas with standard repairs, the IAR and brave semantics allow for tractable query answering.

Our second contribution is to establish connections with abstract argumentation frameworks (AFs). More precisely, we show that every prioritized KB with only binary conflicts naturally corresponds to a preference-based AF [23]. To handle general prioritized KBs, we need preference-based set-based AFs (SETAFs), which we introduce as a natural extension of SETAFs [24]. This correspondence enables us to compare repairs and extensions. We determine that Pareto-optimal repairs are precisely the stable extensions of the corresponding preference-based (SET)AF, and under reasonable assumptions, also coincide with the preferred extensions. To establish the latter result, we prove a technically challenging result about symmetric preference-based SETAFs that we believe is of independent interest. Globally-optimal and completion-optimal repairs correspond to proper subsets of the stable extensions, but do not at present have any analog in the argumentation setting. The argumentation connection situates optimal repairs within a broader context and lays the foundations for importing ideas and results from the argumentation literature. Indeed, our third contribution is to propose a new notion of grounded repair, directly inspired by grounded extensions from argumentation. We show that the (unique) grounded repair is contained in the intersection of Pareto-optimal repairs. As the grounded repair can be computed in polynomial time from the dataset and conflicts, it yields a tractable approximation of the Pareto variant of the IAR semantics for the considered DLs. Moreover, we show that it is more productive than the recently proposed Elect semantics [25], [26]. These advantages motivate us to take a closer look at the computational properties of the grounded semantics. We prove in particular a matching Plower bound and show how the semantics can be computed via the well-founded semantics of logic programs.

Proofs of all results are provided in the appendix.

2 Preliminaries↩︎

Even if many of our results apply to more general settings, our focus is on description logic (DL) knowledge bases, and we will in particular consider the DL-Lite\(_{\mathsf{core}}\) and DL-Lite\(^{\mathcal{H}}_\mathsf{horn}\)dialects of the DL-Lite family.

Syntax. A DL knowledge base (KB) \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\) consists of an ABox \(\mathcal{A}\) and a TBox \(\mathcal{T}\), both constructed from a set \(\mathsf{N_{C}}\)of concept names (unary predicates), a set of \(\mathsf{N_{R}}\)of role names (binary predicates), and a set \(\mathsf{N_{I}}\)of individuals (constants). The ABox (dataset) consists of a finite number of concept assertions of the form \(A(a)\) and role assertions of the form \(R(a,b)\), where \(A \in \mathsf{N_{C}}\), \(R \in \mathsf{N_{R}}\), \(a,b \in \mathsf{N_{I}}\). The TBox (ontology) consists of a set of axioms whose form depends on the DL in question. In DL-Lite\(_{\mathsf{core}}\), TBox axioms are concept inclusions \(B\sqsubseteq C\) built according to the following grammar, where \(A\in \mathsf{N_{C}}\) and \(R\in \mathsf{N_{R}}\): \[B := A \mid \exists S,\quad C:= B \mid \neg B,\quad S:= R \mid R^-.\]

DL-Lite\(^{\mathcal{H}}_\mathsf{horn}\) extends DL-Lite\(_{\mathsf{core}}\) with role inclusions of the form \(S\sqsubseteq Q\) where \(Q:= S \mid \neg S\) and concept inclusions of the form \(B_1\sqcap\dots\sqcap B_n\sqsubseteq C\).

Semantics. An interpretation has the form \(\mathcal{I}= (\Delta^{\mathcal{I}}, \cdot^{\mathcal{I}})\), where \(\Delta^{\mathcal{I}}\) is a non-empty set and \(\cdot^{\mathcal{I}}\) maps each \(A \in \mathsf{N_{C}}\) to \(A^{\mathcal{I}} \subseteq \Delta^{\mathcal{I}}\), each \(R \in \mathsf{N_{R}}\) to \(R^{\mathcal{I}} \subseteq \Delta^{\mathcal{I}} \times \Delta^{\mathcal{I}}\), and each \(a \in \mathsf{N_{I}}\) to \(a^{\mathcal{I}} \in \Delta^{\mathcal{I}}\). The function \(\cdot^{\mathcal{I}}\) is straightforwardly extended to general concepts and roles, e.g. \((\neg B_1)^{\mathcal{I}}= \Delta^{\mathcal{I}}\setminus B_1^{\mathcal{I}}\), \((B_1\sqcap B_2)^{\mathcal{I}}= B_1^{\mathcal{I}}\cap B_2^\mathcal{I}\), \((R^{-})^{\mathcal{I}}=\{(c,d) \mid (d,c) \in R^{\mathcal{I}}\}\) and \((\exists Q)^{\mathcal{I}}=\{c \mid \exists d:\, (c,d) \in Q^{\mathcal{I}}\}\). An interpretation \(\mathcal{I}\) satisfies \(G \sqsubseteq H\) if \(G^{\mathcal{I}} \subseteq H^{\mathcal{I}}\); it satisfies \(A(a)\) (resp. \(R(a,b)\)) if \(a^{\mathcal{I}} \in A^{\mathcal{I}}\) (resp. \((a^{\mathcal{I}},b^{\mathcal{I}})\in R^{\mathcal{I}}\)). We call \(\mathcal{I}\) a model of \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\) if \(\mathcal{I}\) satisfies all axioms in \(\mathcal{T}\) and assertions in \(\mathcal{A}\). A KB \(\mathcal{K}\)is consistent if it has a model; otherwise it is inconsistent. We say that an ABox \(\mathcal{A}\) is \(\mathcal{T}\)-consistent if the KB \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\) is consistent.

Queries. A first-order (FO) query is a first-order logic formula whose atoms are built using the predicate symbols in \(\mathsf{N_{C}}\cup \mathsf{N_{R}}\) and constants in \(\mathsf{N_{I}}\). We will focus on the subclass of conjunctive queries (CQs) which take the form \(q(\vec{x})=\exists \vec{y} \, \psi(\vec{x},\vec{y})\), where \(\psi\) is a conjunction of atoms of the forms \(A(t)\) or \(R(t,t')\) whose terms are either variables from \(\vec{x} \cup \vec{y}\) or individuals. When a CQ consists of a single atom, we called it an instance query (IQ). A query without free variables is called Boolean, and we refer to Boolean CQs as BCQs. A Boolean query \(q\) is satisfied by an interpretation \(\mathcal{I}\), written \(\mathcal{I}\models q\), iff \(q\) is satisfied in \(\mathcal{I}\) according to standard first-order logic semantics; \(q\) is entailed by a KB \(\mathcal{K}\), written \(\mathcal{K}\models q\), iff \(\mathcal{I}\models q\) for every model \(\mathcal{I}\) of \(\mathcal{K}\). Henceforth, when we speak of a (Boolean) query, without specifying the type of query, we mean a (Boolean) CQ.

3 Querying Inconsistent Prioritized KBs↩︎

An inconsistent KB entails every Boolean query under the standard semantics. Several inconsistency-tolerant semantics have been defined to obtain meaningful answers in this context (see [9] for a survey). Most of these semantics are based on the notion of repairs, which correspond to the different ways of restoring consistency by minimally removing some assertions.

Definition 1 (Repair). An ABox repair* of a KB \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\), or repair for short, is an inclusion-maximal \(\mathcal{T}\)-consistent subset of \(\mathcal{A}\). The set of repairs of \(\mathcal{K}\) is denoted by \(\mathit{SRep}(\mathcal{K})\).*

Another central notion is that of conflicts, which are the minimal subsets of assertions that contradict the TBox.

Definition 2 (Conflict). A conflict* of a KB \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\), is a minimal \(\mathcal{T}\)-inconsistent subset of \(\mathcal{A}\). The set of all conflicts of \(\mathcal{K}\) is denoted by \(\mathit{Conf}(\mathcal{K})\) and can be represented as a conflict hypergraph whose vertices are assertions and whose hyperedges are the conflicts.*

To simplify the presentation, we assume throughout the paper that the ABox does not contain any assertion that is inconsistent with the TBox, i.e., every conflict contains at least two assertions. Note that self-contradictory assertions do not occur in any repair, and such assertions can be readily identified and removed using existing reasoning algorithms.

In the database setting, [18] defined three notions of optimal repairs based on a priority relation over facts, which expresses preferences between conflicting facts. Such a relation could e.g.represent expert knowledge of how to resolve certain kinds of conflicts or be learned from manual conflict resolution [27], [28]. We recast these notions in the KB setting.

Definition 3 (Priority relation, completion). Given a KB \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\), a priority relation* \(\succ\) for \(\mathcal{K}\) is an acyclic binary relation over the assertions of \(\mathcal{A}\) such that if \(\alpha\succ\beta\), then there exists \(C\in\mathit{Conf}(\mathcal{K})\) such that \(\{\alpha,\beta\}\subseteq C\). A priority relation \(\succ\) is total iff for all \(\alpha\neq\beta\), if there exists \(C\in\mathit{Conf}(\mathcal{K})\) such that \(\{\alpha,\beta\}\subseteq C\), then \(\alpha\succ\beta\) or \(\beta\succ\alpha\). A completion of \(\succ\) is a total priority relation \(\succ'\;\supseteq \;\,\succ\).*

Definition 4 (Prioritized KB). A prioritized KB* is a pair \((\mathcal{K}, \succ)\) consisting of a KB \(\mathcal{K}\) and priority relation \(\succ\) for \(\mathcal{K}\). The notation \(\mathcal{K}_\succ\) will be used as shorthand for \((\mathcal{K}, \succ)\).*

Definition 5 (Optimal repairs). Consider a prioritized KB \(\mathcal{K}_\succ\) with \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\), and let \(\mathcal{A}' \in \mathit{SRep}(\mathcal{K})\).

A Pareto improvement* of \(\mathcal{A}'\) (w.r.t. \(\succ\)) is a \(\mathcal{T}\)-consistent \(\mathcal{A}''\subseteq\mathcal{A}\) such that there exists \(\beta\in\mathcal{A}''\setminus\mathcal{A}'\) such that \(\beta\succ\alpha\) for every \(\alpha\in\mathcal{A}'\setminus\mathcal{A}''\).*
A global improvement* of \(\mathcal{A}'\) (w.r.t. \(\succ\)) is a \(\mathcal{T}\)-consistent \(\mathcal{A}''\subseteq\mathcal{A}\) such that \(\mathcal{A}''\neq\mathcal{A}'\) and for every \(\alpha\in\mathcal{A}'\setminus\mathcal{A}''\), there exists \(\beta\in\mathcal{A}''\setminus\mathcal{A}'\) such that \(\beta\succ\alpha\).*

The repair \(\mathcal{A}'\) is a:

**Pareto-optimal repair of \(\mathcal{K}_\succ\)* if there is no Pareto improvement of \(\mathcal{A}'\) w.r.t.\(\succ\).*
**Globally-optimal repair of \(\mathcal{K}_\succ\)* if there is no global improvement of \(\mathcal{A}'\) w.r.t.\(\succ\).*
**Completion-optimal repair of \(\mathcal{K}_\succ\)* if \(\mathcal{A}'\) is a globally-optimal repair of \(\mathcal{K}_{\succ'}\), for some completion \(\succ'\) of \(\succ\).*

We denote by \(\mathit{GRep}(\mathcal{K}_\succ)\), \(\mathit{PRep}(\mathcal{K}_\succ)\) and \(\mathit{CRep}(\mathcal{K}_\succ)\) the sets of globally-, Pareto-, and completion-optimal repairs.

[18] showed the following relation between optimal repairs: \[\mathit{CRep}(\mathcal{K}_\succ)\subseteq \mathit{GRep}(\mathcal{K}_\succ)\subseteq \mathit{PRep}(\mathcal{K}_\succ)\subseteq \mathit{SRep}(\mathcal{K}).\] They also show that \(\mathcal{A}'\) is a completion-optimal repair iff it can be obtained by the following greedy procedure: while some assertion has not been considered, pick an assertion that is maximal w.r.t. \(\succ\) among those not yet considered, and add it to the current set if it does not lead to a contradiction.

Example 1. Consider the prioritized KB \(\mathcal{K}_\succ\) given on Figure 1.

Figure 1: Prioritized KB example. \mathcal{T} formalizes knowledge about animal groups and \mathcal{A} gives information about individuals a and b. An arrow from \alpha to \beta indicates that \alpha\succ\beta while a dotted line indicates a conflict without priority between assertions. — Figure 1: Prioritized KB example. \(\mathcal{T}\) formalizes knowledge about animal groups and \(\mathcal{A}\) gives information about individuals \(a\) and \(b\). An arrow from \(\alpha\) to \(\beta\) indicates that \(\alpha\succ\beta\) while a dotted line indicates a conflict without priority between assertions.

The sets of optimal repairs of \(\mathcal{K}_\succ\) are as follows. \[\begin{align} \mathit{CRep}(\mathcal{K}_\succ\!)\!=&\{\! \{\mathsf{Rattler}(a), \mathsf{Carnivorous}(a), \mathsf{EatMeat}(a,b)\!\},\\& \phantom{\{}\{\mathsf{Boa}(a), \mathsf{Carnivorous}(a), \mathsf{EatMeat}(a,b)\}\! \}\\ \mathit{GRep}(\mathcal{K}_\succ\!)\!=&\mathit{CRep}(\mathcal{K}_\succ)\cup\{ \{ \mathsf{Mammal}(a), \mathsf{Oviparous}(a), \\& \quad\quad\quad\quad \mathsf{Carnivorous}(a), \mathsf{EatMeat}(a,b)\} \}\\ \mathit{PRep}(\mathcal{K}_\succ\!)\!=&\mathit{GRep}(\mathcal{K}_\succ)\cup\{\\& \{\mathsf{Rattler}(a), \mathsf{Herbivorous}(a), \mathsf{EatPlant}(a,b)\},\\& \{\mathsf{Boa}(a), \mathsf{Herbivorous}(a), \mathsf{EatPlant}(a,b)\},\\& \{ \mathsf{Mammal}(a), \mathsf{Oviparous}(a), \\& \phantom{\{}\mathsf{Herbivorous}(a), \mathsf{EatPlant}(a,b)\}\! \} \end{align}\] \(\mathit{SRep}(\mathcal{K})\) additionally contains repairs with \(\mathsf{Stone}(b)\) instead of the \(\mathsf{EatPlant}(a,b)\) or \(\mathsf{EatMeat}(a,b)\) assertions.

We next introduce the three natural inconsistency-tolerant semantics based upon repairs. The AR semantics is arguably the most natural and well-known semantics and requires that a query be entailed from every repair of the KB. The IAR semantics is a more cautious semantics that evaluates queries over the intersection of all repairs. Finally, the brave semantics is the most adventurous semantics, returning yes to queries that are entailed by some repair.

Definition 6 (AR, IAR and brave semantics). For \(\text{X}\in\{\text{C},\text{G},\text{P},\text{S}\}\), a prioritized KB \(\mathcal{K}_\succ\) entails a query \(q\) under

**X-AR semantics, written \(\mathcal{K}_\succ \models_{\text{AR}}^{X} q\),

iff \(\langle \mathcal{T},\mathcal{A}'\rangle\models q\) for every \(\mathcal{A}'\in\mathit{XRep}(\mathcal{K}_\succ)\);
**X-IAR semantics, written \(\mathcal{K}_\succ \models_{\text{IAR}}^{X} q\),

iff \(\langle \mathcal{T},\mathcal{A}^{\cap}\rangle \models q\) where \(\mathcal{A}^{\cap}=\bigcap_{\mathcal{A}'\in\mathit{XRep}(\mathcal{K}_\succ)}\mathcal{A}'\);
**X-brave semantics, written \(\mathcal{K}_\succ \models_{\text{brave}}^{X} q\),

iff \(\langle \mathcal{T},\mathcal{A}' \rangle\models q\) for some \(\mathcal{A}'\in\mathit{XRep}(\mathcal{K}_\succ)\).

We remark that these semantics are related as follows: \[\mathcal{K}_\succ \models_{\text{IAR}}^{X} q \Rightarrow \mathcal{K}_\succ \models_{\text{AR}}^{X} q \Rightarrow \mathcal{K}_\succ \models_{\text{brave}}^{X} q.\]

Example 2 (Ex. 1 cont’d). Considering the different semantics based upon completion-optimal repairs, we observe that

\(\mathcal{K}_\succ\models_{\text{IAR}}^{C}\mathsf{Carnivorous}(a)\),
\(\mathcal{K}_\succ\models_{\text{AR}}^{C}\mathsf{Snake}(a)\) but \(\mathcal{K}_\succ\not\models_{\text{IAR}}^{C}\mathsf{Snake}(a)\),
\(\mathcal{K}_\succ\models_{\text{brave}}^{C}\mathsf{Boa}(a)\) but \(\mathcal{K}_\succ\not\models_{\text{AR}}^{C}\mathsf{Boa}(a)\).

If we consider now AR semantics for the different kinds of optimal repairs, we find that

\(\mathcal{K}_\succ\models_{\text{AR}}^{C}\mathsf{Snake}(a)\) but \(\mathcal{K}_\succ\not\models_{\text{AR}}^{G}\mathsf{Snake}(a)\),
\(\mathcal{K}_\succ\models_{\text{AR}}^{G}\mathsf{Carnivorous}(a)\) but \(\mathcal{K}_\succ\not\models_{\text{AR}}^{P}\mathsf{Carnivorous}(a)\),
\(\mathcal{K}_\succ\models_{\text{AR}}^{P}\mathsf{Eat}(a,b)\) but \(\mathcal{K}_\succ\not\models_{\text{AR}}^{S}\mathsf{Eat}(a,b)\).

4 Complexity Analysis↩︎

In this section, we analyze the data complexity of the central reasoning tasks related to optimal repairs.

4.1 Overview↩︎

We define the problems and complexity classes we consider as well as some relevant properties of DL languages.

Problems. Given a prioritized KB \(\mathcal{K}_\succ\) and a type of repairs \(\text{X}\in\{\text{C},\text{G},\text{P},\text{S}\}\), repair checking (isRep) is deciding whether a set of assertions belongs to \(\mathit{XRep}(\mathcal{K}_\succ)\); AR (resp. IAR, brave) entailment (AR, IAR, brave) is deciding whether \(\mathcal{K}_\succ\) entails a given BCQ under X-AR (resp. X-IAR, X-brave) semantics; uniqueness (unique) is deciding whether \(|\mathit{XRep}(\mathcal{K}_\succ)|=1\); and enumeration (enum) is enumerating all elements of \(\mathit{XRep}(\mathcal{K}_\succ)\).

Complexity classes. All of the complexity results stated in this paper are for the data complexity measure, i.e., the complexity is with respect to the size of \(\mathcal{A}\), with \(\mathcal{T}\) and \(q\) treated as fixed (hence of constant size).

For decision problems, we will refer to the following complexity classes: \(\mathsf{AC}^{0}\) is the class of problems that can be solved by a uniform family of cicuits of constant depth and polynomial-size, with unbounded-fanin AND and OR gates; P is the class of problems solvable in polynomial time; NP is the class of problems solvable in non-deterministic polynomial time; \(\Sigma^{p}_{2}\) is the class of problems solvable in non-deterministic polynomial time with access to an NP oracle; coNP(resp. \(\Pi^{p}_{2}\)) is the class of problems whose complement is in NP(resp. \(\Sigma^{p}_{2}\)). These classes are related as follow: \(\mathsf{AC}^{0}\subset\mathrm{\small P}\subseteq\mathrm{\small NP}\subseteq\Sigma^{p}_{2}\) and \(\mathsf{AC}^{0}\subset\mathrm{\small P}\subseteq \text{co\mathrm{\small NP}} \subseteq\Pi^{p}_{2}\). It is widely believed that all of the inclusions are proper.

For enumeration problems, we will use the following classes: TotalP is the class of enumeration problems that can be solved in polynomial time in \(n+m\) where \(n\) is the input size and \(m\) the output size; DelayP is the class of enumeration problems that can be solved by an algorithm such that the delay between the \(k^{th}\) and the \(k+1^{th}\) solution is bounded by a polynomial in the input size; IncP is the class of enumeration problems that can be solved by an algorithm such that the delay between the \(k^{th}\) and the \(k+1^{th}\) solution is bounded by a polynomial in the size of the input and \(k\). These classes are related as follow: \(\mathrm{\small DelayP}\subseteq \mathrm{\small IncP}\subseteq \mathrm{\small TotalP}\). If the decision problem associated to an enumeration problem is NP-hard, then the enumeration problem is not in \(\mathrm{\small TotalP}\).

Results. Table 1 presents an overview of the complexity results for DL-Lite. However, since most of the results hold for some DLs outside the DL-Lite family, we will state them for DLs that satisfy some of the following properties:

BoundConf: the size of conflicts is bounded;
BinConf: conflicts have size at most two;
PolyBCQ: polynomial time BCQ entailment;
PolyCons: polynomial time consistency checking.

The most commonly considered DL-Lite dialects, such as DL-Lite\(_{\mathsf{core}}\)and DL-Lite\(_{\mathcal{R}}\)(the basis for OWL 2 QL), satisfy all of these properties, while DL-Lite\(^{\mathcal{H}}_\mathsf{horn}\) satisfies all except BinConf(the size of conflicts is bounded by the number of concept and role names occurring in the TBox).

Table 1: Data complexity overview. Lower bounds hold for . Upper bounds hold for except those noted with \(^\ast\) which hold only for . Results for the \(\reps{\Kmc}\) case are stated (or are straightforward consequences of results) in[9], [12], [22].\(^\ddagger\) in if \(\succ\) is transitive \(^\dagger\) if \(\succ\) is score-structured \(^\ast\) for KBs with a score-structured priority relation \(\succ\) (see Section [sec:sec:trans] for the definition)
\(\reps{\Kmc}\)	\(\preps{\Kmc_\succ}\)	\(\greps{\Kmc_\succ}\)	\(\creps{\Kmc_\succ}\)
in	in	-c	in
-c	-c	-c	-c
in	-c	-c	-c
in	-c	-c	-c
in	-c	-c\(^\ddagger\)	in
\(\delayp^{\ast}\)	not \(\totalp^\dagger\)	not \(\totalp^\dagger\)	\(\delayp^{\ast}\)

1pt

4.2 Query Entailment↩︎

We start by establishing the complexity of repair checking and BCQ entailment under the various semantics.

The upper bounds are stated in the following theorem and can be proven by adapting existing results from databases and inconsistency-tolerant OMQA (recall that proofs of all results are provided in the appendix). Observe that this result applies to all DLs satisfying PolyCons and PolyBCQ, which includes prominent Horn DLs like \(\mathcal{EL}\) and Horn-\(\mathcal{SHIQ}\).

theoremPropComplexityRepairCheckEntailment For DLs satisfying PolyCons, repair checking is in coNP for globally-optimal repairs, in P for Pareto- or completion-optimal repairs.

For DLs satisfying PolyCons and PolyBCQ, G-AR and G-IAR entailment are in \(\Pi^{p}_{2}\), G-brave entailment in \(\Sigma^{p}_{2}\), P-AR, P-IAR, C-AR and C-IAR entailment are in coNP, and P-brave and C-brave entailment in NP.

For Pareto-optimal and completion-optimal repairs, coNP-hardness (resp.NP-hardness) of AR and IAR (resp.brave) IQ entailment in DL-Lite\(_{\mathsf{core}}\) follow from the special case where the priority relation is given by priority levels, for which it is known the three families of optimal repairs we consider coincide [29]. The following theorem establishes the remaining lower bounds.

theoremThmHardnessGlobal In DL-Lite\(_{\mathsf{core}}\), repair checking is coNP-hard for globally-optimal repairs, G-AR and G-IAR entailment are \(\Pi^{p}_{2}\)-hard, and G-brave entailment \(\Sigma^{p}_{2}\)-hard, even for IQs.

4.3 Uniqueness and Enumeration↩︎

We now turn our attention to the problems of deciding uniqueness and enumerating repairs. Note that in the case of classical repairs, deciding whether \(|\mathit{SRep}(\mathcal{K})|=1\) amounts to checking whether \(\mathcal{K}\) is consistent (recall our assumption that all self-contradictory assertions have been removed).

As observed by [22] in the database setting, classical repairs correspond to the maximal independent sets (MISs) of the conflict hypergraph. It is known that MIS enumeration for graphs is in \(\mathrm{\small DelayP}\) [30], while for hypergraphs with bounded-size hyperedges, the problem is in \(\mathrm{\small IncP}\) [31], [32]. Since the conflict hypergraph can be tractably computed for DLs with bounded-size conflicts, enumeration of \(\mathit{SRep}(\mathcal{K})\) is in IncP for DLs with bounded conflicts, and in DelayPfor DLs with binary conflicts.

[21] and [22] provide intractability results for unique and enum in the case of globally- and Pareto-optimal repairs of databases with functional dependencies. Their proofs do not transfer to DL-Lite KBs, but via different proofs, we can establish analogous results in our context.

theoremThmUniqueness Uniqueness is coNP-complete for Pareto-optimal repairs, \(\Pi^{p}_{2}\)-complete for globally-optimal repairs. Upper bounds hold for DLs satisfying PolyCons. Lower bounds hold for DL-Lite\(_{\mathsf{core}}\).

Corollary 1. Enumeration of Pareto-optimal or globally-optimal repairs is not in TotalP for DL-Lite\(_{\mathsf{core}}\).

[21] provide an algorithm which, given an arbitrary conflict hypergraph and a priority relation, decides uniqueness for completion-optimal repairs in polynomial time. Hence deciding whether \(|\mathit{CRep}(\mathcal{K}_\succ)|=1\) is in P for DLs with bounded conflicts, since in this case the conflict hypergraph can be computed in polynomial time. [22] describe an algorithm that enumerates completion-optimal repairs with polynomial delay for conflict graphs. It follows that for DLs with binary conflicts, enumeration of completion-optimal repairs is in DelayP. The case of completion-optimal repairs with non-binary conflicts remains open.

4.4 Case of Transitive Priority Relations↩︎

A natural case to consider is when the priority relation is transitive. This occurs in particular when the priority relation captures the relative reliability of the facts.

Definition 7. A priority relation is transitive* if \(\alpha_1\succ\dots\succ\alpha_n\) and \(\{\alpha_1,\alpha_n\}\subseteq C\in\mathit{Conf}(\mathcal{K})\) implies \(\alpha_1\succ\alpha_n\).*

[21] proved that when the priority relation is transitive, deciding uniqueness for globally-optimal repairs can be done in polynomial time when the conflict hypergraph is given. This result is applicable to all DLs for which the conflict hypergraph is computable in polynomial time. A natural question is whether any of our other problems become easier if we assume \(\succ\) is transitive. We found that this is not the case, although the transitivity requirement makes the lower bounds proofs more involved. In particular, we can no longer use the coNP-hardness proof for uniqueness to derive that the enumeration of globally-optimal repairs is not in TotalP, but instead show this via the coNP-hardness of deciding whether a given set of ABoxes is exactly \(\mathit{GRep}(\mathcal{K}_\succ)\).

theoremThmTransitivity When \(\succ\) is transitive, uniqueness is in P for globally-optimal repairs and DLs satisfying BoundConf. All other lower bounds in Table 1 still hold for DL-Lite\(_{\mathsf{core}}\).

Score-structured priority relations. An interesting special case of transitive priority relation arises when every assertion \(\alpha\) is assigned a natural number called its score (or priority level) \(s(\alpha)\), which induces a priority relation as follows: for every pair of assertions \(\alpha\) and \(\beta\) that belongs to a conflict, \(\alpha\succ\beta\) if and only if \(s(\alpha)>s(\beta)\). [22] call such a priority relation score-structured and show that deciding whether a priority is score-structured is in P and that if \(\succ\) is score-structured, \(\mathit{CRep}(\mathcal{K}_\succ)= \mathit{GRep}(\mathcal{K}_\succ)= \mathit{PRep}(\mathcal{K}_\succ)\). This relation was also given in [17], [29] where it is shown that they further coincide with another notion of preferred repairs directly defined from ABoxes partitioned into priority levels.

For score-structured priorities, the complexity of all decision problems is the same as in the case of completion-optimal repairs, with the lower bounds shown in [29]. By contrast, for enumeration, it follows from the algorithm for enumerating score-structured priority repairs of [22] that enumeration is in IncP for DLs with bounded conflicts and consistency checking in P.

5 Preference-Based Argumentation↩︎

In preparation for the following section, we recall the basics of argumentation frameworks and previously studied extensions with preferences and collective attacks. We also prove some new results (Theorems [thm:symm-coherent], [thm:SymPAFChar], [thm:StrongSymmSETAF], and [psetaf-coh]).

5.1 Argumentation Frameworks↩︎

We consider finite argumentation frameworks. Argumentation frameworks over an infinite set of arguments have also been studied in the literature but finiteness is an ordinary assumption and is made for all results we recall or extend here.

Definition 8. An argumentation framework* (AF) is a pair \((\mathit{Args},\rightsquigarrow)\) where \(\mathit{Args}\) is a finite set of arguments and \(\rightsquigarrow\, \subseteq \mathit{Args}\times \mathit{Args}\) is the attack relation. When \((\alpha, \beta)\! \in \rightsquigarrow\), we say that \(\alpha\) attacks \(\beta\), alternatively denoted by \(\alpha \rightsquigarrow\beta\).*

We recall some commonly used notation and terminology, letting \((\mathit{Args}, \rightsquigarrow)\) be the considered AF and \(A \subseteq \mathit{Args}\). We use \(A^+=\{\beta \mid \alpha \rightsquigarrow\beta \text{ for some }\alpha \in A\}\) to denote the set of arguments attacked by arguments from \(A\). We say that \(A\) defends \(\gamma\in \mathit{Args}\) (or, \(\gamma\) is defended by \(A\)) iff \(\{\beta \mid \beta \rightsquigarrow\gamma\} \subseteq A^+\). A set \(A \subseteq \mathit{Args}\) is conflict-free if \(A \cap A^+ = \emptyset\). The characteristic function \(\Gamma_{F}:2^{\mathit{Args}} \mapsto 2^{\mathit{Args}}\) of \(F=(\mathit{Args}, \rightsquigarrow)\) is defined as follows: \(\Gamma_{F}(A) = \{\alpha \mid \alpha \text{ is defended by } A\}\). A set \(A \subseteq \mathit{Args}\) is admissible if it is conflict-free and \(A \subseteq \Gamma_{F}(A)\). Argumentation semantics are usually based upon extensions, intended to capture coherent sets of arguments. We recall some prominent notions of extension:

Definition 9. Let \(F=(\mathit{Args}, \rightsquigarrow)\). Then \(E \subseteq \mathit{Args}\) is a:

**complete extension* iff \(E\) is conflict-free and \(E=\Gamma_{F}(E)\);*
**grounded extension* iff \(E\) is the \(\subseteq\)-minimal complete extension, or equivalently, the least fixpoint of \(\Gamma_{F}\);*
**preferred extension* iff \(E\) is a \(\subseteq\)-maximal admissible set;*
**stable extension* iff \(E^+ = \mathit{Args}\setminus E\).*

While every stable extension is a preferred extension, the converse does not hold in general [33]. The term coherent designates AFs for which these two notions coincide (i.e.every preferred extension is stable). Coherence is viewed as a desirable property, and several sufficient conditions for coherence have been identified. In particular:

Definition 10. An AF \((\mathit{Args}, \rightsquigarrow)\) is symmetric* iff \(\rightsquigarrow\) is symmetric and irreflexive.*

Theorem 1. [34] Every symmetric AF is coherent.

5.2 Enriching AFs with Preferences↩︎

There has been significant interest in extending AFs to allow for preferences between arguments [23], [35].

Definition 11. A preference-based argumentation framework* (PAF) is a triple \((\mathit{Args},\rightsquigarrow, \succ)\), where \(\mathit{Args}\) and \(\rightsquigarrow\) are as before, and \(\succ\) is an acyclic binary relation over \(\mathit{Args}\) (called the preference relation). Symmetric PAFs are obtained by requiring (\(\mathit{Args}, \rightsquigarrow\)) to be symmetric.*

It is typical to assume that the preference relation \(\succ\) is transitive. This is a reasonable assumption, but for the sake of generality, the preceding definition does not impose this.

The standard way of defining the semantics of PAFs is via reduction to (plain) AFs:

Definition 12. Given a PAF \((\mathit{Args},\rightsquigarrow, \succ)\), the corresponding AF* is \((\mathit{Args}, \rightsquigarrow_\succ)\), where \(\alpha \rightsquigarrow_\succ \beta\) iff \(\alpha \rightsquigarrow\beta\) and \(\beta \not \succ \alpha\). A subset \(E \subseteq \mathit{Args}\) is a stable (resp.preferred, grounded, complete) extension of a PAF \((\mathit{Args},\rightsquigarrow, \succ)\) iff it is a stable (resp.preferred, grounded, complete) extension of the corresponding AF.*

While alternative reductions have been proposed in [36] and [23], all of these reductions coincide for symmetric PAFs, which is the case that will interest us here.

Theorem 2. [36]Every symmetric PAF with a transitive preference relation is coherent.

We generalize the preceding result by showing that transitivity is not required:

theoremthmSymmCoherent Every symmetric PAF is coherent.

Theorem [thm:SymPAFChar] gives a characterization of AFs that correspond to symmetric PAFs. It generalizes the strict acyclicity condition characterizing the so-called conflict+preference AFs [37] that requires for any cycle \(\alpha_1 \rightsquigarrow\alpha_2\rightsquigarrow\dots\rightsquigarrow\alpha_n\rightsquigarrow\alpha_1\) that \(\alpha_1 \rightsquigarrow\alpha_n\rightsquigarrow\dots\rightsquigarrow\alpha_2\rightsquigarrow\alpha_1\).

theoremthmSymPAFChar For every AF \(F=(\mathit{Args}, \rightsquigarrow)\), the following statements are equivalent.

\(F\) is the corresponding AF of some symmetric PAF.
For any cycle \(\alpha_1 \rightsquigarrow\alpha_2\rightsquigarrow\dots\rightsquigarrow\alpha_n\rightsquigarrow\alpha_1\), there exists \((j,i)\in\{(1,2),\dots,(n-1,n),(n,1)\}\) with \(\alpha_i\rightsquigarrow\alpha_j\).

5.3 Set-Based Argumentation Frameworks↩︎

Another well-studied extension of AFs is to allow collective attacks, in which a set of arguments together form an attack [24], [38].

Definition 13. A set-based argumentation framework* (SETAF) is a pair \((\mathit{Args}, \rightsquigarrow)\) where \(\mathit{Args}\) is a finite set of arguments, and \(\rightsquigarrow\, \subseteq (2^{\mathit{Args}}\setminus \{\emptyset\}) \times \mathit{Args}\) is the attack relation. We’ll write \(S \rightsquigarrow\alpha\) to mean \((S, \alpha)\! \in \rightsquigarrow\).*

When working with SETAFs, we define \(A^+\) as \(\{\beta \mid S \rightsquigarrow\beta \text{ for some }S \subseteq A\}\) and say \(A\) defends \(\beta\) iff \(A^+\cap S \neq \emptyset\) whenever \(S \rightsquigarrow\beta\). The definitions of characteristic function, conflict-free, admissibility, different types of extensions, and coherence for SETAFs are the same as for AFs but using these modified notions of defeated and defended arguments.

Symmetric SETAFs were recently defined as follows:

Definition 14. [39] A SETAF \((\mathit{Args}, \rightsquigarrow)\) is symmetric* if the following two conditions hold: (Symm-1) if \(S \rightsquigarrow\beta\) and \(\alpha \in S\), then \(S' \cup \{\beta\}\rightsquigarrow\alpha\) for some \(S'\), and (Irr) there is no \(S \rightsquigarrow\alpha\) with \(\alpha \in S\).*

Unfortunately, [39] show their definition does not preserve the nice properties of symmetric AFs. In particular:

Theorem 3. Some symmetric SETAFs are not coherent.

We propose an alternative, and we believe quite natural, notion of symmetric SETAF, which we term ‘strongly symmetric’ to distinguish it from the preceding notion:

Definition 15. A SETAF \((\mathit{Args}, \rightsquigarrow)\) is strongly symmetric* if it satisfies (Irr) and (Symm-2): for every attack \(S \rightsquigarrow\beta\) and every \(\alpha\in S\), we have \(S\setminus\{\alpha\}\cup\{\beta\}\rightsquigarrow\alpha\).*

With our definition, symmetry implies coherence:

theoremthmStrongSymmSETAF Strongly symmetric SETAFs are coherent.

5.4 Adding Preferences to SETAFs↩︎

It is natural to combine the preceding two extensions, but to the best of our knowledge, this combination has not yet been considered. We propose the following definition:

Definition 16. A preference-based set-based argumentation framework* (PSETAF) is a triple \((\mathit{Args},\rightsquigarrow, \succ)\), where \((\mathit{Args},\rightsquigarrow)\) is a SETAF, and \(\succ\) is an acyclic binary relation over \(\mathit{Args}\), called the preference relation.*

To define the semantics of PSETAFs, we give a reduction to SETAFs, which generalizes the one for PAFs:

Definition 17. Given a PSETAF \((\mathit{Args},\rightsquigarrow, \succ)\), its corresponding SETAF is \((\mathit{Args},\rightsquigarrow_\succ)\), where the relation \(\rightsquigarrow_\succ \subseteq (2^{\mathit{Args}} \setminus \{\emptyset\}) \times \mathit{Args}\) is defined as follows: \(S \rightsquigarrow_\succ \alpha\) iff \(S \rightsquigarrow\alpha\) and \(\alpha \not \succ \beta\) for every \(\beta \in S\). A subset \(E \subseteq \mathit{Args}\) is a stable (resp.preferred, grounded, complete) extension of a PSETAF \((\mathit{Args},\rightsquigarrow, \succ)\) iff it is a stable (resp.preferred, grounded, complete) extension of the corresponding SETAF.

We will focus on strongly symmetric PSETAFs:

Definition 18. A PSETAF \((\mathit{Args},\rightsquigarrow, \succ)\) is strongly symmetric* if the SETAF \((\mathit{Args},\rightsquigarrow)\) is strongly symmetric.*

The following result lifts Theorem 2 to PSETAFs. The proof is quite intricate, and we leave open whether the same result holds without the transitivity assumption:

theoremthmPSETAF Every strongly symmetric PSETAF with a transitive preference relation is coherent.

6 Linking Prioritized KBs and PSETAFs↩︎

This section places optimal repairs into a broader context by exhibiting a tight relationship between optimal repairs and extensions of argumentation frameworks. The argumentation connection is then exploited to define a new kind of prioritized repair with favourable computational properties.

Each prioritized KB naturally gives rise to a PSETAF in which the ABox assertions play the role of arguments, and the attack relation captures the conflicts.

Definition 19. Given a prioritized KB \(\mathcal{K}_\succ\) with \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\), the associated PSETAF is \(F_{\mathcal{K}, \succ}= (\mathcal{A}, \rightsquigarrow_{\mathcal{K}}, \succ)\), where \(\rightsquigarrow_{\mathcal{K}} = \{(C \setminus \{\alpha\}, \alpha) \mid C \in \mathit{Conf}(\mathcal{K}), \alpha \in C\}\).

Remark 4. Recall that we assume the ABoxes do not contain self-conflicting assertions, hence \(C \setminus \{\alpha\} \neq \emptyset\). If we choose not to make this assumption, we should omit such assertions when constructing the PSETAF, i.e., using \(\mathcal{A}\setminus \{\alpha \mid \langle \mathcal{T}, \{\alpha\}\rangle \models \bot\}\) for the set of arguments and only considering \(C \in \mathit{Conf}(\mathcal{K})\) with \(|C| \geq 2\) to construct \(\rightsquigarrow_{\mathcal{K}}\).

In this section, results are formulated for arbitrary KBs, except where otherwise noted.

6.1 Optimal Repairs vs. PSETAF Extensions↩︎

Now that we have translated prioritized KBs into argumentation frameworks, it is possible to compare preferred repairs and extensions. The following theorem shows that Pareto-optimal repairs correspond precisely to stable extensions.

theoremthmstable \(\mathcal{A}' \subseteq \mathcal{A}\) is a Pareto-optimal repair of \(\mathcal{K}_\succ = (\langle \mathcal{T}, \mathcal{A}\rangle, \succ)\) iff \(\mathcal{A}'\) is a stable extension of \(F_{\mathcal{K}, \succ}\).

Observe that our translation always produces strongly symmetric PSETAFs, which makes it possible to transfer Theorem [psetaf-coh] when the priority relation is transitive.

theoremthmTransCoherent If \(\succ\) is a transitive priority relation, then the PSETAF \(F_{\mathcal{K}, \succ}\) is coherent.

Theorems [tstable] and [trans-coherent] together show that for transitive \(\succ\), Pareto-repairs coincide also with preferred extensions.

For KBs which contain only binary conflicts (e.g. core DL-Lite dialects), the resulting PSETAF is actually a PAF, so we can drop the transitivity requirement:

Theorem 5. For every prioritized KB \(\mathcal{K}_\succ\) such that \(\mathcal{C}\in \mathit{Conf}(\mathcal{K})\) implies \(|\mathcal{C}|=2\), \(F_{\mathcal{K}, \succ}\) is coherent. Thus, \(\mathcal{A}' \in \mathit{PRep}(\mathcal{K}_\succ)\) iff \(\mathcal{A}'\) is a preferred extension of \(F_{\mathcal{K}, \succ}\).

Note that it follows from Theorem [tstable] that globally-optimal and completion-optimal repairs correspond to proper subsets of the stable extensions of \(F_{\mathcal{K}, \succ}\), but they do not at present have any analog in the argumentation setting. For a (SET)AF \(F\) that corresponds to a (strongly) symmetric P(SET)AF \(P\), it is possible to define new types of extensions that will correspond to globally- and completion-optimal repairs of a KB having \(P\) for associated P(SET)AF and to import results from the prioritized KB setting. In particular, when \(F\) is an AF that respects the conditions of Theorem [thm:SymPAFChar], we can adapt the algorithms for completion-optimal repairs to tractably enumerate a non-empty subset of the stable/preferred extensions of \(F\), while enumerating its stable/preferred extensions is not in TotalP in general.

6.2 Grounded Semantics for Prioritized KBs↩︎

We next turn to the relationship between grounded extensions and optimal repair semantics. We start by clarifying the situation for the simplest case, in which there are no preferences (cf.[40] for a similar result in a different but related setting).

theoremthmGroundedNoPref Let \(\mathcal{K}=\langle \mathcal{T}, \mathcal{A}\rangle\) be a KB, and let \(F_\mathcal{K}\) be the SETAF corresponding to \(F_{\mathcal{K}, \succ_\emptyset}\) (with \(\succ_\emptyset\) the empty relation). Then the grounded extension of \(F_\mathcal{K}\) coincides with the intersection of the repairs of \(\mathcal{K}\).

For prioritized KBs, we can use Theorem [tstable] and the fact that every stable extension is a complete extension to relate grounded extensions with Pareto-optimal repairs:

theoremthmGroundedPareto If \(\mathcal{G}\) is the grounded extension of \(F_{\mathcal{K}, \succ}\), then \(\mathcal{G}\subseteq \mathcal{B}\) for every \(\mathcal{B}\in \mathit{PRep}(\mathcal{K}_\succ)\).

Thus, the grounded extension contains only assertions common to all Pareto-optimal repairs. It may not contain all such assertions, as the following example illustrates:

Example 3. Consider a prioritized KB \(\mathcal{K}_\succ\) in which \(\mathit{Conf}(\mathcal{K})=\{\{\alpha,\beta\},\{\alpha,\gamma\},\{\beta,\gamma\},\{\gamma,\delta\}\}\) and where \(\succ\) contains \(\alpha\succ\gamma\), \(\beta\succ\gamma\), and \(\gamma\succ\delta\). Then \(\delta\) appears in the two Pareto-optimal repairs of \(\mathcal{K}_\succ\), which are \(\{\alpha,\delta\}\) and \(\{\beta,\delta\}\), while the grounded extension of \(F_{\mathcal{K}, \succ}\) is \(\emptyset\).

We propose to use the grounded extension to define a new inconsistency-tolerant semantics for prioritized KBs:

Definition 20. A query \(q\) is entailed from \(\mathcal{K}_\succ\) under grounded semantics, denoted \(\mathcal{K}_\succ \models_{GR} q\), iff \(\langle \mathcal{T}, \mathcal{G}\rangle \models q\), where \(\mathcal{G}\) is the grounded extension of \(F_{\mathcal{K}, \succ}\).

As follows from Theorem [ground-pareto], our new semantics provides an under-approximation of the P-IAR semantics:

Theorem 6. For every prioritized KB \(\mathcal{K}_\succ\) and query \(q\): \(\mathcal{K}_\succ \models_{GR} q\) implies \(\mathcal{K}_\succ \models_{\text{IAR}}^{P} q\).

Importantly, since the grounded extension of a (SET)AF can be computed in polynomial time, this semantics allows for tractable query answering in some relevant settings.

Theorem 7. Let \(\mathcal{L}\) be a DL satisfying BoundConf, PolyBCQ and PolyCons. Then the problem of BCQ entailment over \(\mathcal{L}\)-KBs under grounded semantics is in Pw.r.t.data complexity.

Corollary 2. For DL-Lite\(^{\mathcal{H}}_\mathsf{horn}\)KBs, BCQ entailment under grounded semantics is in Pw.r.t.data complexity.

The grounded semantics can be compared to another recently proposed semantics for prioritized KBs, the Elect semantics, defined for KBs with binary conflicts by [25] then generalized for non-binary conflicts [26]. Elect evaluates queries over a set of elected assertions and is tractable for DLs for which computing the conflicts and BCQ entailment can be done in polynomial time w.r.t. data complexity.

Definition 21. [26] An assertion \(\alpha\in\mathcal{A}\) is elected* iff for every \(C\in\mathit{Conf}(\mathcal{K})\), if \(\alpha\in C\), then there exists \(\beta\in C\) such that \(\alpha\succ\beta\). The set of elected assertions is denoted by \(\mathit{Elect}(\mathcal{K}_\succ)\).*

The grounded semantics is more productive than Elect, i.e., is a more precise under-approximation of P-IAR.

theoremthmElect \(\mathit{Elect}(\mathcal{K}_\succ)\subseteq \mathcal{G}\) where \(\mathcal{G}\) is the grounded extension of \(F_{\mathcal{K}, \succ}\).

Example 4. Consider a prioritized KB \(\mathcal{K}_\succ\) in which \(\mathit{Conf}(\mathcal{K})=\{\{\alpha,\beta\},\{\beta,\gamma\}\}\) and where \(\succ\) contains \(\alpha\succ\beta\) and \(\beta\succ\gamma\). Then \(\mathit{Elect}(\mathcal{K}_\succ)=\{\alpha\}\) while \(\mathcal{G}=\{\alpha,\gamma\}\). Indeed, \(\alpha\in\mathcal{G}\) and \(\gamma\) is defended by \(\{\alpha\}\) in the AF corresponding to \(F_{\mathcal{K}, \succ}\), so \(\gamma\in \mathcal{G}\).

Our next result establishes that reasoning under grounded semantics is P-complete in the settings of Theorem 7.

theoremthmGroundedHardness IQ entailment under grounded semantics is P-hard w.r.t. data complexity for DL-Lite\(_{\mathsf{core}}\).

Dung ([33]) observed that the grounded extension can be computed via the well-founded semantics of a simple logic program. The following lemma generalizes this result to \(k\)-SETAFs, i.e., SETAFs for which \(S \rightsquigarrow\beta\) implies \(|S| \leq k\).

Theorem 8. Let \(F=(\mathit{Args},\rightsquigarrow)\) be a \(k\)-SETAF. Then \(\alpha\) is in the grounded extension of \(F\) iff \(\mathtt{acc}(\alpha)\) belongs to the well-founded model of the following normal logic program: \[\begin{align} &\{\mathtt{def}(x) \!\leftarrow\! \mathtt{att}_i\!(y_1\!,.., y_i,x), \! \mathtt{acc}(y_1),\!...,\!\mathtt{acc}(y_i)\! \mid \!1 \!\leq \! i \leq\! k\} \\ &\cup \{\mathtt{acc}(x) \leftarrow \mathtt{arg}(x), \neg\mathtt{def}(x)\} \cup \{\mathtt{arg}(\alpha) \mid \alpha \in \mathit{Args}\} \\ &\cup \{\mathtt{att}_i(\alpha_1, \ldots, \alpha_i, \beta) \leftarrow \, \mid \{\alpha_1, \ldots, \alpha_i\} \rightsquigarrow\beta\} \end{align}\]

Intuitively, the preceding logic program computes the sets of defeated (\(\mathtt{def}\)) and accepted (\(\mathtt{acc}\)) arguments starting from the original sets of arguments (\(\mathtt{arg}\)) and attacks (\(\mathtt{att}_i\) encodes \(i\)-ary attacks). By adding rules to compute conflicts and populate the attack relations \(\mathtt{att}_i\), we can show that the grounded extension of \(F_{\mathcal{K}, \succ}\) can be computed via logic programming. While stated for DL-Lite\(^{\mathcal{H}}_\mathsf{horn}\), the next theorem holds for any ontology (or constraint) language for which inconsistency can be characterized by a finite set of BCQs.

theoremWfhorn For every DL-Lite\(^{\mathcal{H}}_\mathsf{horn}\)TBox \(\mathcal{T}\), there exists a normal logic program \(\Pi_\mathcal{T}\) such that for every ABox \(\mathcal{A}\), priority relation \(\succ\) for \(\mathcal{K}=\langle \mathcal{T}, \mathcal{A}\rangle\), and assertion \(\alpha\), the following are equivalent:

\(\alpha\) belongs to the grounded extension of the PSETAF \(F_{\mathcal{K}, \succ}\)
\(\mathtt{acc}(id(\alpha))\) belongs to the well-founded model of \(\Pi_\mathcal{T}\cup \{\gamma \leftarrow \, \mid \gamma \in \mathcal{A}_{id}\} \cup \{ \mathtt{pref}(id(\alpha), id(\beta)) \leftarrow \, \mid \alpha \succ \beta\}\),

where \(\mathcal{A}_{id}\) is obtained from \(\mathcal{A}\) by adding an extra argument to every assertion \(\beta\) containing a unique id, denoted \(id(\beta)\).

As the well-founded semantics is implemented in logic programming systems like XSB [41], the preceding theorem presents a method for implementing grounded semantics. Alternatively, the grounded extension can be naturally under-approximated by fixing \(d>0\) and considering \(\Gamma_{F}^d(\emptyset)\) rather than the least fixpoint of \(\Gamma_{F}\). The logic program from Theorem [thm:wfgrnd] can be modified to yield a non-recursive stratified program that computes \(\Gamma^d_{F_{\mathcal{K}, \succ}}(\emptyset)\), which in turn can be expressed as a first-order (\(\sim\) SQL) query and evaluated using a relational database system.

Our complexity results are similar to those obtained for prioritized databases with functional dependencies [18], [21], [22]. Compared to this work, we additionally consider IAR and brave semantics, study the impact of transitivity on all reasoning tasks, and establish connections with argumentation.

Inconsistency-tolerant semantics based on other kinds of preferred repairs have been investigated both in the database and DL or Datalog\(^\pm\) contexts, often with a focus on repairs that have maximal cardinality or weight [42]–[45]. However, such global optimality criteria lead to a higher computational complexity (typically \(\Delta^P_2[O(log\;n)]\)-hard). By contrast, [17] show that for preferred repairs based on priority levels and set-inclusion (corresponding to optimal repairs in the score-structured case), BCQ entailment remains in the first level of the polynomial hierarchy for DL-Lite. Our results show that even if the priority relation over facts is not score-structured, and not even transitive, these computational properties are retained for Pareto- and completion-optimal repairs.

When \(\succ\) is score-structured, we can compare the grounded extension and the intersection of optimal repairs to the proposals of [46] for selecting a single preferred \(\mathcal{T}\)-consistent subset of the ABox. In particular, the non-defeated repair is the union of the intersections of the repairs of \(S_1, S_1\cup S_2, \dots, S_1\cup\dots \cup S_n\), where \(S_1,\dots, S_n\) is a partition of \(\mathcal{A}\) into priority levels. Since Elect coincides with non-defeated semantics for score-structured priorities [26], the non-defeated repair is included in the grounded extension by Theorem [thm:elect]; as the priority relation in Example 4 is score-structured, the inclusion may be strict. Another proposal is the prioritized inclusion-based non-defeated repair, which coincides with the intersection of the optimal repairs. The grounded extension thus lies between the non-defeated and prioritized inclusion-based non-defeated repairs. Other proposals are either included in non-defeated, or are not sound approximations of the intersection of the optimal repairs. For partially preordered ABoxes, [26] propose to go beyond Elect by intersecting the optimal repairs w.r.t. the score-structured priorities obtained by extending the original partial preorder into a total preorder. Interestingly, the obtained set of assertions corresponds exactly to the intersection of the completion-optimal repairs of the prioritized KB underpinned by the partially preordered KB (cf.appendix D).

Argumentation frameworks derived from inconsistent KBs have been considered before. Arguments are generally defined as pairs of a support (subset of the KB) and a conclusion (consequence of the support), with various attack relations (see e.g., [35], [47]). A series of papers starting with [40] links argumentation and inconsistency-tolerant querying of KBs, where the support of the argument is a subset of the ABox, the conclusion is a conjunction of facts entailed from the support and \(\mathcal{T}\), and \(\alpha\) attacks \(\beta\) iff the conclusion of \(\alpha\) is \(\mathcal{T}\)-inconsistent with the support of \(\beta\) (in some papers, the argument consists of a whole derivation sequence, not just the support and conclusion). Stable and preferred extensions of such AFs correspond to repairs in the following sense: every such extension contains all those arguments whose supports are included in some particular repair. The work by [48] shows that it is possible to use a preference relation over facts to define notions of optimal extensions for AFs induced by inconsistent KBs in this fashion, and observe that such extensions correspond to optimal repairs. While touching on similar topics, an essential difference between this line of work and our own lies in the definition of the AF. Indeed, in the AFs of Croitoru et al., even if we group together arguments with the same supports, we would still have an exponential number of arguments. By contrast, our translation can be carried out in polynomial time under reasonable assumptions, enabling us to import tractability results from argumentation to OMQA. Moreover, since we use assertions as arguments, each priority relation yields a preference relation over arguments, enabling a transparent reduction to preference-based (SET)AFs. [48] do not discuss any connections to preference-based, nor set-based AFs, and our results on the equivalence between Pareto-optimal repairs and stable and preferred extensions of P(SET)AFs do not follow from their results.

8 Conclusion and Future Work↩︎

We have explored the problem of how to repair and query inconsistent KBs while taking into account a priority relation over facts. By leveraging connections to database repairs and abstract argumentation, we obtained a number of novel results for our setting, while at the same time contributing new results and research questions to these two areas.

After importing the notions of Pareto-, globally-, and completion-optimal repairs into the OMQA setting, our first contribution was a data complexity study that showed, unsurprisingly, that reasoning with optimal repairs is typically intractable and more challenging than for classical repairs. Nevertheless, there are several cases which are ‘only’ NP/ coNP, which suggests that it may be interesting to devise practical SAT-based procedures, as has been successfully done for some other forms of repair [17]. It would also be relevant to implement and experiment our proposed grounded semantics as well as the first-order approximations we suggested. Our complexity study could be expanded to include further ontology languages as well as the combined complexity measure.

In order to provide an elegant translation of prioritized KBs to argumentation frameworks, we were naturally led to consider preference-based (SET)AFs. We believe that the new results we established in Section 5, in particular, Theorem [psetaf-coh], should be of interest to the argumentation community. Moreover, the connections we established between extensions of PSETAFs and repairs of prioritized KBs motivate a more detailed study of PSETAFs (a concrete open question is whether Theorem [psetaf-coh] holds in the absence of transitivity). Furthermore, this correspondence could be leveraged to explore new notions of extension for (strongly) symmetric P(SET)AFs inspired by completion- or globally-optimal repairs, or to design benchmarks for (P)(SET)AFs via a translation from inconsistent KBs.

An important question that has not yet been satisfactorily answered in the database literature is which of the three forms of optimal repair is most natural, independently of their computational costs. While we do not claim to provide a definitive answer to this question, we believe that our result showing that Pareto-optimal repairs coincide with stable extensions (and often also preferred extensions) speaks to the interest of adopting Pareto-optimal repairs. We should emphasize that while phrased for KBs, the connection between Pareto-optimal repairs and stable / preferred extensions holds equally well for databases with denial constraints (such as functional dependencies). Moreover, the tractable grounded semantics we proposed can be applied not just to KBs but also to prioritized databases.

Acknowledgements↩︎

This work was supported by Camille Bourgaux’s CNRS PEPS grant and the ANR AI Chair INTENDED.

9 Proofs for Section 4 ↩︎

Proof. For repair checking, the proofs are similar to the database case. Verifying that \(\mathcal{A}'\) belongs to \(\mathit{SRep}(\mathcal{K})\) can be done in polynomial time. Then if \(\mathcal{A}'\in\mathit{SRep}(\mathcal{K})\), to show that \(\mathcal{A}'\) is not globally-optimal, it suffices to guess a global improvement of \(\mathcal{A}'\) and verify it in polynomial time; to show that \(\mathcal{A}'\) is not Pareto-optimal, it suffices to check for each assertion \(\beta\notin\mathcal{A}'\) whether \(\mathcal{A}''=\mathcal{A}'\cup\{\beta\}\setminus\{\alpha\mid \beta\succ\alpha\}\) is \(\mathcal{T}\)-consistent, which implies that it is a Pareto improvement of \(\mathcal{A}'\). Finally, to check that \(\mathcal{A}'\) is completion-optimal, we can use the greedy procedure described in Section 3 by restricting the choice of facts to the intersection of \(\mathcal{A}'\) and the not-yet-considered facts that are maximal w.r.t. \(\succ\).

For AR, IAR and brave entailment, we use the following standard algorithms to decide (non-)entailment. The upper complexity bounds then follow from the complexity of repair checking and BCQ entailment. To decide \(\mathcal{K}_\succ\not\models_{\text{AR}}^{X} q\) (resp.\(\mathcal{K}_\succ\models_{\text{brave}}^{X} q\)), guess \(\mathcal{A}'\in\mathit{XRep}(\mathcal{K}_\succ)\) such that \(\langle \mathcal{T},\mathcal{A}'\rangle\not\models q\) (resp. \(\langle \mathcal{T},\mathcal{A}'\rangle\models q\)). To decide \(\mathcal{K}_\succ\not\models_{\text{IAR}}^{X} q\), guess a set of assertions \(\mathcal{B}=\{\alpha_1,\dots,\alpha_n\}\subseteq\mathcal{A}\) such that \(\langle \mathcal{T},\mathcal{A}\setminus\mathcal{B}\rangle\not\models q\) together with \(\mathcal{A}'_1,\dots,\mathcal{A}'_n\) in \(\mathit{XRep}(\mathcal{K}_\succ)\) such that \(\alpha_i\notin\mathcal{A}'_i\) for \(1\leq i\leq n\). Since \(\bigcap_{\mathcal{A}'\in\mathit{XRep}(\mathcal{K}_\succ)}\mathcal{A}'\subseteq \mathcal{A}\setminus\mathcal{B}\), this implies that \(\mathcal{K}_\succ\not\models_{\text{IAR}}^{X}q\). ◻

Given a propositional formula \(\varphi\) and a partial valuation \(\nu\) of its variables, \(\nu(\varphi)\) denotes the formula obtained by replacing each variable \(x\) in the domain of \(\nu\) by \(\nu(x)\) in \(\varphi\).

Proof. coNP-hardness of globally-optimal repair checking. We show coNP-hardness of repair checking for globally-optimal repairs by reduction from UNSAT. Let \(\Phi=c_1\wedge \dots\wedge c_k\) be a conjunction of clauses \(c_1,\dots, c_k\) over variables \(x_1,\dots, x_n\). We define a KB \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\) and a priority relation \(\succ\) over \(\mathcal{A}\) as follows. \[\begin{align} \mathcal{T}=&\{\exists P^-\sqsubseteq\neg\exists N^-, \exists P\sqsubseteq\neg \exists\mathit{Unsat}^-, \exists N\sqsubseteq\neg \exists\mathit{Unsat}^-,\exists\mathit{Block}_\exists^-\sqsubseteq\neg \exists P^-, \exists\mathit{Block}_\exists^-\sqsubseteq\neg \exists N^-\} \\ &\cup\{ \mathit{Exist}\sqsubseteq\neg\exists\mathit{Block}_\exists, \mathit{Exist}\sqsubseteq\neg\exists\mathit{Unsat} \}\\ \mathcal{A}=&\{\mathit{Unsat}(a,c_i)\mid 1\leq i\leq k\}\cup\{P(c_i,x_j)\mid x_j\in c_i\}\cup\{N(c_i,x_j)\mid \neg x_j\in c_i\}\\ &\cup\{\mathit{Block}_\exists(a,x_j)\mid 1\leq j\leq n\}\cup\{\mathit{Exist}(a)\} \end{align}\] \[\begin{align} \mathit{Exist}(a)&\succ\mathit{Block}_\exists(a,x_j)\\ \mathit{Block}_\exists(a,x_j)&\succ P(c_i,x_j)\\ \mathit{Block}_\exists(a,x_j)&\succ N(c_i,x_j)\\ P(c_i,x_j)&\succ \mathit{Unsat}(a,c_i)\\ N(c_i,x_j)&\succ \mathit{Unsat}(a,c_i) \end{align}\]

We show that \(\Phi\) is satisfiable iff \(\mathcal{A}'=\{\mathit{Unsat}(a,c_i)\mid 1\leq i\leq k\}\cup\{\mathit{Block}_\exists(a,x_j)\mid 1\leq j\leq n\}\notin\mathit{GRep}(\mathcal{K}_\succ)\). It is easy to verify that \(\mathcal{A}'\in\mathit{SRep}(\mathcal{K})\), i.e., is an inclusion-maximal \(\mathcal{T}\)-consistent subset of \(\mathcal{A}\).

(\(\Rightarrow\)) Assume that \(\Phi\) is satisfiable and let \(\nu\) be a valuation of \(x_1,\dots,x_n\) that satisfies \(\Phi\). Let \[\mathcal{A}_\nu=\{P(c_i,x_j)\mid x_j\in c_i, \nu(x_j)=\mathsf{true}\}\cup\{N(c_i,x_j)\mid \neg x_j\in c_i, \nu(x_j)=\mathsf{false}\}\cup\{\mathit{Exist}(a)\}.\] Since \(\nu\) satisfies \(\Phi\), then \(\nu\) satisfies every clause \(c_i\) so every \(c_i\) has an outgoing \(P\) or \(N\) edge in \(\mathcal{A}_\nu\). It is easy to see that \(\mathcal{A}_\nu\) is \(\mathcal{T}\)-consistent (since no \(x_j\) has both a \(P\) and a \(N\) incoming edge). Moreover, since \(\mathit{Exist}(a)\succ\mathit{Block}_\exists(a,x_j)\), \(P(c_i,x_j)\succ \mathit{Unsat}(a,c_i)\), and \(N(c_i,x_j)\succ \mathit{Unsat}(a,c_i)\), it follows that \(\mathcal{A}_\nu\) is a global improvement of \(\mathcal{A}'\), so \(\mathcal{A}'\notin\mathit{GRep}(\mathcal{K}_\succ)\).
(\(\Leftarrow\)) Assume that \(\mathcal{A}'\notin\mathit{GRep}(\mathcal{K}_\succ)\). There exists a global improvement \(\mathcal{A}_\nu\) of \(\mathcal{A}'\), i.e., a \(\mathcal{T}\)-consistent \(\mathcal{A}_\nu\subseteq \mathcal{A}\), \(\mathcal{A}_\nu\neq\mathcal{A}'\), such that for every \(\alpha\in\mathcal{A}'\setminus\mathcal{A}_\nu\), there exists \(\beta\in\mathcal{A}_\nu\setminus\mathcal{A}'\) such that \(\beta\succ\alpha\). Assume for a contradiction that for every \(x_j\), \(\mathit{Block}_\exists(a,x_j)\notin \mathcal{A}'\setminus\mathcal{A}_\nu\). Since \(\mathcal{A}_\nu\neq\mathcal{A}'\) and \(\mathcal{A}'\) is a maximal \(\mathcal{T}\)-consistent subset of \(\mathcal{A}\), then \(\mathcal{A}'\not\subseteq\mathcal{A}_\nu\), so there exists \(\alpha\in\mathcal{A}'\setminus\mathcal{A}_\nu\). Thus there exists \(c_i\) such that \(\mathit{Unsat}(a,c_i)\in\mathcal{A}'\setminus\mathcal{A}_\nu\). By construction of \(\succ\), there must then be some \(P(c_i,x_j)\) or \(N(c_i,x_j)\) in \(\mathcal{A}_\nu\). However, since we assumed \(\mathit{Block}_\exists(a,x_j)\notin \mathcal{A}'\setminus\mathcal{A}_\nu\), then \(\mathcal{A}_\nu\) is \(\mathcal{T}\)-inconsistent. It follows that there exists \(x_j\) such that \(\mathit{Block}_\exists(a,x_j)\in \mathcal{A}'\setminus\mathcal{A}_\nu\). By construction of \(\succ\), it follows that \(\mathit{Exist}(a)\in\mathcal{A}_\nu\). Since \(\mathcal{A}_\nu\) is \(\mathcal{T}\)-consistent, there is thus no \(\mathit{Block}_\exists(a,x_j)\) and no \(\mathit{Unsat}(a,c_i)\) in \(\mathcal{A}_\nu\). Hence for every \(i\), \(\mathit{Unsat}(a,c_i)\in\mathcal{A}'\setminus\mathcal{A}_\nu\), so there must be some \(P(c_i,x_j)\) or \(N(c_i,x_j)\) in \(\mathcal{A}_\nu\). Let \(\nu\) be the valuation of \(x_1,\dots, x_n\) such that \(\nu(x_j)=\mathsf{true}\) iff \(P(c_i,x_j)\in\mathcal{A}_\nu\). Since \(\mathcal{A}_\nu\) is \(\mathcal{T}\)-consistent, then every \(x_j\) has only \(P\) or \(N\) incoming edges. It follows that if \(P(c_i,x_j)\in\mathcal{A}_\nu\), then \(x_j\in c_i\) and \(\nu(x_j)=\mathsf{true}\) so \(\nu(c_i)=\mathsf{true}\), and if \(N(c_i,x_j)\in\mathcal{A}_\nu\), then \(\neg x_j\in c_i\) and \(\nu(x_j)=\mathsf{false}\) so \(\nu(c_i)=\mathsf{true}\). Hence \(\nu\) satisfies \(\Phi\).

\(\Pi^{p}_{2}\)-hardness of G-AR and G-IAR IQ entailment. We show \(\Pi^{p}_{2}\)-hardness of G-AR and G-IAR IQ entailment by reduction from 2QBF. Let \(\Psi=\forall x_1\dots x_n\exists x_{n+1}\dots x_{n+m} \Phi\) where \(\Phi=c_1\wedge \dots\wedge c_k\) is a conjunction of clauses over variables \(x_1,\dots, x_n, x_{n+1},\dots, x_{n+m}\). We assume that every variable occurs in both positive and negative literals (this is w.l.o.g. since \(\Psi'\) obtained by replacing \(\Phi\) by \(\Phi'=c_1\wedge \dots\wedge c_{k}\wedge (x_1\vee\neg x_1)\wedge\dots\wedge (x_{m+n}\vee\neg x_{m+n})\) is valid iff \(\Psi\) is valid). We define a KB \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\) and a priority relation \(\succ\) over \(\mathcal{A}\) as follows. \[\begin{align} \mathcal{T}=&\{\exists P^-\sqsubseteq\neg\exists N^-, \exists P\sqsubseteq\neg \exists\mathit{Unsat}^-, \exists N\sqsubseteq\neg \exists\mathit{Unsat}^-\}\cup\{\exists\mathit{Block}_Q^-\sqsubseteq\neg \exists P^-, \exists\mathit{Block}_Q^-\sqsubseteq\neg \exists N^-\mid Q\in\{\exists,\forall\} \}\\& \cup\{ \mathit{Exist}\sqsubseteq\neg\exists\mathit{Block}_\exists, \mathit{Exist}\sqsubseteq\neg\exists\mathit{Unsat}, \mathit{Univ}\sqsubseteq\neg\exists\mathit{Block}_\forall, \mathit{Exist}\sqsubseteq\neg\mathit{Univ}, \mathit{Univ}\sqsubseteq \neg\mathit{NoUniv} \}\\ &\cup\{\exists\mathit{Block}_\exists\sqsubseteq\neg\exists\mathit{Block}_\forall\}\\ \mathcal{A}=&\{\mathit{Unsat}(a,c_i)\mid 1\leq i\leq k\}\cup\{P(c_i,x_j)\mid x_j\in c_i\}\cup\{N(c_i,x_j)\mid \neg x_j\in c_i\}\\ &\cup\{\mathit{Block}_\forall(a,x_j)\mid 1\leq j\leq n\}\cup\{\mathit{Block}_\exists(a,x_j)\mid n+1\leq j\leq n+m\}\cup\{\mathit{Exist}(a),\mathit{Univ}(a), \mathit{NoUniv}(a)\} \end{align}\] \[\begin{align} \mathit{Block}_{\forall}(a,x_j) &\succ \mathit{Block}_{\exists}(a, x_{j'})\\ \mathit{Block}_{Q}(a,x_j) &\succ P(c_i, x_j)&Q\in\{\exists,\forall\}\\ \mathit{Block}_{Q}(a,x_j) &\succ N(c_i, x_j)&Q\in\{\exists,\forall\}\\ P(c_i,x_j) &\succ \mathit{Unsat}(a,c_i)\\ N(c_i,x_j) &\succ \mathit{Unsat}(a,c_i)\\ \mathit{Exist}(a)&\succ\mathit{Univ}(a) \end{align}\] We show that \(\mathcal{K}_\succ\models_{\text{AR}}^{G}\mathit{NoUniv}(a)\) (resp. \(\mathcal{K}_\succ\models_{\text{IAR}}^{G}\mathit{NoUniv}(a)\)) iff \(\Psi\) is valid.

(\(\Rightarrow\)) Assume that \(\Psi\) is not valid: there exists a valuation \(\nu_\forall\) of \(x_1,\dots,x_n\) such that for every valuation \(\nu_\exists\) of \(x_{n+1},\dots,x_{n+m}\), \(\nu_\forall(\nu_\exists(\Phi))\) evaluates to false. Let \[\begin{align} \mathcal{A}_\forall=& \{\mathit{Univ}(a)\}\cup\{\mathit{Block}_\exists(a,x_j)\mid n+1\leq j\leq n+m\}\\& \cup\{P(c_i,x_j)\mid 1\leq j\leq n, x_j\in c_i, \nu_\forall(x_j)=\mathsf{true}\}\\& \cup\{N(c_i,x_j)\mid 1\leq j\leq n, \neg x_j\in c_i, \nu_\forall(x_j)=\mathsf{false}\} \\& \cup\{\mathit{Unsat}(a,c_i)\mid \nu_\forall(c_i)\text{ does not evaluate to }\mathsf{true}\}. \end{align}\] It is easy to check that \(\mathcal{A}_\forall\) is a repair. In particular, every \(x_j\) has only incoming \(P\) or \(N\) edges in \(\mathcal{A}_\forall\) and every \(c_i\) has an incoming \(\mathit{Unsat}\) edge only if it has no outgoing \(P\) or \(N\) edges, so \(\mathcal{A}_\forall\) is \(\mathcal{T}\)-consistent. Moreover, it is not possible to add an assertion from \(\mathcal{A}\setminus\mathcal{A}_\forall\) while staying \(\mathcal{T}\)-consistent. In particular, the \(P\) and \(N\) assertions that involve some \(x_j\) with \(j>n\) are in conflict with \(\mathit{Block}_\exists(a,x_j)\in\mathcal{A}_\forall\). We show that \(\mathcal{A}_\forall\in\mathit{GRep}(\mathcal{K}_\succ)\), which implies \(\mathcal{K}_\succ\not\models_{\text{AR}}^{G}\mathit{NoUniv}(a)\) (and thus \(\mathcal{K}_\succ\not\models_{\text{IAR}}^{G}\mathit{NoUniv}(a)\)).

Assume for a contradiction that there exists a \(\mathcal{T}\)-consistent \(\mathcal{A}'\subseteq\mathcal{A}\), \(\mathcal{A}'\neq\mathcal{A}_\forall\), such that for every \(\alpha\in\mathcal{A}_\forall\setminus\mathcal{A}'\), there exists \(\beta\in\mathcal{A}'\setminus\mathcal{A}_\forall\) such that \(\beta\succ\alpha\). If \(\mathit{Exist}(a)\notin\mathcal{A}'\), then \(\mathcal{A}'\) contains \(\mathit{Univ}(a)\) by construction of \(\succ\). Since \(\mathit{Univ}(a)\) is inconsistent with the \(\mathit{Block}_\forall(a,x_j)\), then (i) for every \(j\leq n\), \(\mathit{Block}_\forall(a,x_j)\notin\mathcal{A}'\) and (ii) \(\mathcal{A}'\) contains all the \(\mathit{Block}_\exists(a,x_j)\) by construction of \(\succ\). It follows from (ii) that for every \(j>n\), \(x_j\) has no incoming \(P\) or \(N\) edge in \(\mathcal{A}'\), and from (i) that for every \(j\leq n\), \(\mathcal{A}'\) contains the same \(P(c_i,x_j)\) and \(N(c_i,x_j)\) as \(\mathcal{A}_\forall\) by construction of \(\succ\). Hence, by construction of \(\succ\), \(\mathcal{A}'\) contains the same \(\mathit{Unsat}(a,c_i)\) as \(\mathcal{A}_\forall\). It follows that \(\mathcal{A}'=\mathcal{A}_\forall\), which contradicts our assumptions on \(\mathcal{A}'\). Hence \(\mathit{Exist}(a)\in\mathcal{A}'\). Since \(\mathit{Exist}(a)\in\mathcal{A}'\), then \(\mathit{Univ}(a)\notin\mathcal{A}'\), for every \(j>n\), \(\mathit{Block}_\exists(a,x_j)\notin\mathcal{A}'\), and for every \(i\), \(\mathit{Unsat}(a,c_i)\notin\mathcal{A}'\). By construction of \(\succ\), for each \(\mathit{Unsat}(a,c_i)\in\mathcal{A}_\forall\), there must then be some \(P(c_i,x_j)\) or \(N(c_i,x_j)\) in \(\mathcal{A}'\setminus\mathcal{A}_\forall\). Moreover, since \(\Psi\) is not valid, one of these \(P(c_i,x_j)\) or \(N(c_i,x_j)\) in \(\mathcal{A}'\setminus\mathcal{A}_\forall\) is such that \(j\leq n\). Indeed, we otherwise define the valuation \(\nu_\exists\) of \(x_{n+1},\dots,x_{n+m}\) by \(\nu_\exists(x_j)=\mathsf{true}\) iff \(x_j\) has an incoming \(P\) edge in \(\mathcal{A}'\). It is easy to see that \(\nu_\exists\) satisfies all clauses of \(\Phi\) that were not already satisfied by \(\nu_\forall\), so that \(\nu_\exists(\nu_\forall(\Phi))\) evaluates to true. Assume w.l.o.g. that there is \(j\leq n\) such that \(P(c_i,x_j)\in\mathcal{A}'\setminus\mathcal{A}_\forall\). Since \(P(c_i,x_j)\notin\mathcal{A}_\forall\), \(\nu_\forall(x_j)=\mathsf{false}\). Since we assumed that both \(x_j\) and \(\neg x_j\) occur in \(\Phi\), it follows that \(N(c_{i'},x_j)\in\mathcal{A}_\forall\). Hence, since \(\mathcal{A}'\) is \(\mathcal{T}\)-consistent, \(N(c_{i'},x_j)\in\mathcal{A}_\forall\setminus\mathcal{A}'\) so there must be \(\beta\in\mathcal{A}'\) such that \(\beta\succ N(c_{i'},x_j)\). However, every \(\beta\in\mathcal{A}\) such that \(\beta\succ N(c_{i'},x_j)\) is inconsistent with \(P(c_i,x_j)\in\mathcal{A}'\). We obtain a contradiction so there does not exist any global improvement of \(\mathcal{A}_\forall\), and \(\mathcal{A}_\forall\in\mathit{GRep}(\mathcal{K}_\succ)\).
(\(\Leftarrow\)) In the other direction, assume that \(\Psi\) is valid: for every valuation \(\nu_\forall\) of \(x_1,\dots,x_n\), there exists a valuation \(\nu_\exists\) of \(x_{n+1},\dots,x_{n+m}\) such that \(\nu_\forall(\nu_\exists(\Phi))\) evaluates to true. Assume for a contradiction that there exists \(\mathcal{A}'\in\mathit{GRep}(\mathcal{K}_\succ)\) such that \(\mathit{NoUniv}(a)\notin\mathcal{A}'\), i.e., \(\mathit{Univ}(a)\in\mathcal{A}'\) by maximality of \(\mathcal{A}'\). By \(\mathcal{T}\)-consistency of \(\mathcal{A}'\), \(\mathit{Exist}(a)\notin\mathcal{A}'\) and there is no \(\mathit{Block}_{\forall}(a,x_j)\) in \(\mathcal{A}'\). Since \(\mathit{Block}_{\exists}(a,x_j) \succ P(c_i, x_j)\) and \(\mathit{Block}_{\exists}(a,x_j)\succ N(c_i, x_j)\), then \(\{\mathit{Block}_{\exists}(a,x_j)\mid n+1\leq j\leq n+m\}\subseteq\mathcal{A}'\). Finally, since \(P(c_i,x_j) \succ \mathit{Unsat}(a,c_i)\) and \(N(c_i,x_j) \succ \mathit{Unsat}(a,c_i)\), \(\mathcal{A}'\) contains a maximal \(\mathcal{T}\)-consistent subset of the \(P(c_i,x_j)\) and \(N(c_i,x_j)\) with \(j\leq n\), so there exists a valuation \(\nu_\forall\) of \(x_1,\dots,x_n\) such that \[\begin{align} \mathcal{A}'=&\{\mathit{Univ}(a)\}\cup\{\mathit{Block}_{\exists}(a,x_j)\mid n+1\leq j\leq n+m\}\\ &\cup\{P(c_i,x_j)\mid j\leq n, P(c_i,x_j)\in\mathcal{A}, \nu_\forall(x_j)=\mathsf{true}\}\\ &\cup\{N(c_i,x_j)\mid j\leq n, N(c_i,x_j)\in\mathcal{A}, \nu_\forall(x_j)=\mathsf{false}\}\\ &\cup\{\mathit{Unsat}(a,c_i)\mid \nu_\forall(c_i)\text{ does not evaluate to true}\}. \end{align}\]

Since \(\Psi\) is valid, there exists a valuation \(\nu_\exists\) of \(x_{n+1},\dots,x_{n+m}\) such that \(\nu_\forall(\nu_\exists(\Phi))\) evaluates to true. Let \[\begin{align} \mathcal{A}_\nu=&\{\mathit{Exist}(a)\}\cup\{\mathit{Block}_{\forall}(a,x_j)\mid1\leq j\leq n\}\cup\\&\{P(c_i,x_j)\mid j>n,P(c_i,x_j)\in\mathcal{A},\nu_\exists(x_j)=\mathsf{true}\}\cup\\&\{N(c_i,x_j)\mid j>n,N(c_i,x_j)\in\mathcal{A},\nu_\exists(x_j)=\mathsf{false}\}. \end{align}\] Each \(c_i\) such that \(\mathit{Unsat}(a,c_i)\in\mathcal{A}'\) has a \(P\) or \(N\) outgoing edge in \(\mathcal{A}_\nu\) because \(\nu_\forall(\nu_\exists(\Phi))\) evaluates to true and \(\mathit{Unsat}(a,c_i)\in\mathcal{A}'\) only if \(\nu_\forall(c_i)\) does not evaluate to true, so that \(\nu_\exists(c_i)\) evaluates to true. Moreover, \(\mathit{Exist}(a)\succ\mathit{Univ}(a)\), \(\mathit{Block}_{\forall}(a,x_j)\succ\mathit{Block}_{\exists}(a,x_{j'})\), \(\mathit{Block}_{\forall}(a,x_j) \succ P(c_i, x_j)\), \(\mathit{Block}_{\forall}(a,x_j) \succ N(c_i, x_j)\), \(P(c_i,x_j)\succ\mathit{Unsat}(a,c_i)\), and \(N(c_i,x_j)\succ\mathit{Unsat}(a,c_i)\). It follows that \(\mathcal{A}_\nu\) is a global improvement of \(\mathcal{A}'\). We conclude that every globally-optimal repair contains \(\mathit{NoUniv}(a)\), i.e., \(\mathcal{K}_\succ\models_{\text{IAR}}^{G} \mathit{NoUniv}(a)\).

\(\Sigma^{p}_{2}\)-hardness of G-brave IQ entailment. We use the above reduction to show that \(\mathcal{K}_\succ\models_{\text{brave}}^{G}\mathit{Univ}(a)\) iff \(\Psi\) is not valid.

(\(\Rightarrow\)) If \(\Psi\) is valid, the globally-optimal repairs contain \(\mathit{NoUniv}(a)\) so do not contain \(\mathit{Univ}(a)\) and \(\mathcal{K}_\succ\not\models_{\text{brave}}^{G}\mathit{Univ}(a)\).

(\(\Leftarrow\)) If \(\Psi\) is not valid, \(\mathcal{A}_\forall\in\mathit{GRep}(\mathcal{K}_\succ)\) and \(\mathit{Univ}(a)\in\mathcal{A}_\forall\) so \(\mathcal{K}_\succ\models_{\text{brave}}^{G}\mathit{Univ}(a)\). ◻

Proof. Upper bounds. To show that \(|\mathit{XRep}(\mathcal{K}_\succ)|\neq 1\), guess \(\mathcal{A}'\neq\mathcal{A}''\) and check that \(\mathcal{A}'\in\mathit{XRep}(\mathcal{K}_\succ)\) and \(\mathcal{A}''\in\mathit{XRep}(\mathcal{K}_\succ)\). For DLs with polynomial time consistency checking, repair checking is in P for \(X=P\) and in coNP for \(X=G\) by Theorem [Prop:complexityRepairCheckEntailment].

coNP-hardness of uniqueness for Pareto-optimal repairs. We show coNP-hardness of uniqueness for Pareto-optimal repairs by reduction from UNSAT. Let \(\Phi=c_1\wedge \dots\wedge c_k\) be a conjunction of clauses \(c_1,\dots, c_k\) over variables \(x_1,\dots, x_n\). We define a KB \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\) and a priority relation \(\succ\) over \(\mathcal{A}\) as follows. \[\begin{align} \mathcal{T}=&\{\exists P^-\sqsubseteq\neg\exists N^-, \exists P\sqsubseteq\neg \exists\mathit{Unsat}^-, \exists N\sqsubseteq\neg \exists\mathit{Unsat}^-,\exists\mathit{Block}_\exists^-\sqsubseteq\neg \exists P^-, \exists\mathit{Block}_\exists^-\sqsubseteq\neg \exists N^- \} \\ &\cup\{ \mathit{Exist}\sqsubseteq\neg\exists\mathit{Block}_\exists, \mathit{Exist}\sqsubseteq\neg\exists\mathit{Unsat}, \mathit{Exist}\sqsubseteq\neg\mathit{NoExist} \}\\ \mathcal{A}=&\{\mathit{Unsat}(a,c_i)\mid 1\leq i\leq k\}\cup\{P(c_i,x_j)\mid x_j\in c_i\}\cup\{N(c_i,x_j)\mid \neg x_j\in c_i\} \\ &\cup\{\mathit{Block}_\exists(a,x_j)\mid 1\leq j\leq n\} \cup\{\mathit{Exist}(a),\mathit{NoExist}(a)\} \end{align}\] \[\begin{align} \mathit{Unsat}(a,c_i)\succ& \mathit{Exist}(a)\\ \mathit{Exist}(a)\succ&\mathit{Block}_\exists(a,x_j)\\ \mathit{Block}_\exists(a,x_j)\succ& P(c_i,x_j)\\ \mathit{Block}_\exists(a,x_j)\succ& N(c_i,x_j) \end{align}\] Let \(\mathcal{A}'=\{\mathit{NoExist}(a)\}\cup\{\mathit{Block}_\exists(a,x_j)\mid 1\leq j\leq n\}\cup\{\mathit{Unsat}(a,c_i)\mid 1\leq i\leq k\}\). It is easy to check that \(\mathcal{A}'\in\mathit{PRep}(\mathcal{K}_\succ)\): \(\mathcal{A}'\) is \(\mathcal{T}\)-consistent, and it is not possible to add any assertion \(\alpha\in\mathcal{A}\setminus\mathcal{A}'\) to \(\mathcal{A}'\) while staying \(\mathcal{T}\)-consistent without removing an assertion \(\beta\in\mathcal{A}'\) such that \(\alpha\not\succ\beta\). We show that \(\Phi\) is unsatisfiable iff \(|\mathit{PRep}(\mathcal{K}_\succ)|=1\), i.e., \(\mathcal{A}'\) is the unique Pareto-optimal repair.
(\(\Leftarrow\)) Assume that \(\Phi\) is satisfiable: there exists a valuation \(\nu\) that satisfies \(\Phi\). Let \(\mathcal{A}_\nu=\{P(c_i,x_j)\mid x_j\in c_i, \nu(x_j)=\mathsf{true}\}\cup\{N(c_i,x_j)\mid \neg x_j\in c_i, \nu(x_j)=\mathsf{false}\} \cup\{\mathit{Exist}(a)\}\). It is easy to see that \(\mathcal{A}_\nu\) is \(\mathcal{T}\)-consistent since every \(x_j\) has only incoming \(P\) or \(N\) edges. We show that \(\mathcal{A}_\nu\in\mathit{PRep}(\mathcal{K}_\succ)\). It is not possible to add \(\mathit{NoExist}(a)\) without removing \(\mathit{Exist}(a)\) and \(\mathit{NoExist}(a)\not\succ\mathit{Exist}(a)\). Since \(\nu\) satisfies \(\Phi\), every \(c_i\) has an outgoing \(P\) or \(N\) edge in \(\mathcal{A}_\nu\) so it is not possible to add an assertion of the form \(\mathit{Unsat}(a,c_i)\) without removing an assertion of the form \(P(c_i,x_j)\) or \(N(c_i,x_j)\) and \(\mathit{Unsat}(a,c_i)\not\succ P(c_i,x_j)\), \(\mathit{Unsat}(a,c_i)\not\succ N(c_i,x_j)\). It is not possible to add a \(\mathit{Block}_\exists(a,x_j)\) assertion without removing \(\mathit{Exist}(a)\) and \(\mathit{Block}_\exists(a,x_j)\not\succ\mathit{Exist}(a)\). Finally, it is not possible to add \(P(c_i,x_j)\) without removing some \(N(c_{i'},x_j)\) and \(P(c_i,x_j)\not\succ N(c_{i'},x_j)\). Similarly it is not possible to add \(N(c_i,x_j)\). It follows that \(\mathcal{A}_\nu\in\mathit{PRep}(\mathcal{K}_\succ)\) and \(|\mathit{PRep}(\mathcal{K}_\succ)|\geq 2\).
(\(\Rightarrow\)) Assume that there exists a Pareto-optimal repair \(\mathcal{A}''\neq\mathcal{A}'\). Assume for a contradiction that \(\mathit{Exist}(a)\notin\mathcal{A}''\). By maximality, \(\mathit{NoExist}(a)\in\mathcal{A}''\). Moreover, \(\mathcal{A}''\) contains no \(P\) or \(N\) assertions: otherwise, all \(P\) or \(N\) edges incoming in some \(x_j\) could be replaced by \(\mathit{Block}_\exists(a,x_j)\) to obtain a Pareto-improvement of \(\mathcal{A}''\). By maximality, \(\mathcal{A}''\) thus contains all \(\mathit{Block}_\exists\) and \(\mathit{Unsat}\) assertions. We obtain that \(\mathcal{A}''=\mathcal{A}'\), which contradicts our assumption. It follows that \(\mathit{Exist}(a)\in\mathcal{A}''\). Hence \(\mathit{NoExist}(a)\notin\mathcal{A}''\) and there is no \(\mathit{Block}_\exists\) or \(\mathit{Unsat}\) assertions in \(\mathcal{A}''\). Thus the remaining assertions of \(\mathcal{A}''\) form a maximal subset of the \(P\) and \(N\) assertions such that no \(x_j\) has both \(P\) and \(N\) incoming edges. Let \(\nu\) be the valuation of \(x_1,\dots, x_n\) such that \(\nu(x_j)=\mathsf{true}\) iff \(P(x_j)\in\mathcal{A}''\). We show that \(\nu\) satisfies \(\Phi\). Otherwise, there would be a \(c_i\) without \(P\) or \(N\) outgoing edge and \((\mathcal{A}''\setminus\{\mathit{Exist}(a)\})\cup\{\mathit{Unsat}(a,c_i)\}\) would be a Pareto improvement of \(\mathcal{A}''\) since \(\mathit{Unsat}(a,c_i)\succ \mathit{Exist}(a)\). It follows that \(\Phi\) is satisfiable.

\(\Pi^{p}_{2}\)-hardness of uniqueness for globally-optimal repairs. We show \(\Pi^{p}_{2}\)-hardness of uniqueness for globally-optimal repairs by reduction from 2QBF. Let \(\Psi=\forall x_1\dots x_n\exists x_{n+1}\dots x_{n+m} \Phi\) where \(\Phi=c_1\wedge \dots\wedge c_k\) is a conjunction of clauses over variables \(x_1,\dots, x_n, x_{n+1},\dots, x_{n+m}\). We define a KB \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\) and a priority relation \(\succ\) over \(\mathcal{A}\) as follows. \[\begin{align} \mathcal{T}=&\{ \exists P^-\sqsubseteq\neg\exists N^-, \exists P\sqsubseteq\neg \exists\mathit{Unsat}^-, \exists N\sqsubseteq\neg \exists\mathit{Unsat}^-\}\\ &\cup\{\exists P_\forall^-\sqsubseteq\neg\exists N_\forall^-, \exists P_\forall^-\sqsubseteq\neg\exists N^-, \exists P^-\sqsubseteq\neg\exists N_\forall^-\} \\&\cup \{\exists P_\forall\sqsubseteq\neg \exists P, \exists P_\forall\sqsubseteq\neg \exists N, \exists N_\forall\sqsubseteq\neg \exists P, \exists N_\forall\sqsubseteq\neg \exists N\}\\ &\cup\{\exists\mathit{Block}_Q^-\sqsubseteq\neg \exists P^-, \exists\mathit{Block}_Q^-\sqsubseteq\neg \exists N^-\mid Q\in\{\exists, \mathsf{all}\} \}\\ &\cup\{\exists\mathit{Block}_Q^-\sqsubseteq\neg \exists P_\forall^-, \exists\mathit{Block}_Q^-\sqsubseteq\neg \exists N_\forall^-\mid Q\in\{\forall, \mathsf{all}\} \}\\ &\cup\{\exists\mathit{Block}_\exists\sqsubseteq\neg\exists\mathit{Block}_\forall, \exists\mathit{Block}_\forall\sqsubseteq\neg\exists\mathit{Block}_\mathsf{all},\exists\mathit{Block}_\mathsf{all}\sqsubseteq\neg\exists\mathit{Block}_\exists \}\\ &\cup\{\exists\mathit{Block}_Q\sqsubseteq\neg \mathit{Exist}\mid Q\in\{\exists, \mathsf{all}\} \}\\ &\cup\{\exists\mathit{Block}_Q\sqsubseteq\neg \mathit{Univ}, \exists\mathit{Block}_Q\sqsubseteq\neg \exists\mathit{Unsat}\mid Q\in\{\forall, \mathsf{all}\} \}\\ &\cup\{\exists\mathit{Block}_Q\sqsubseteq\neg \mathit{NoExist}\mid Q\in\{\exists, \forall\} \}\\ &\cup\{ \mathit{Exist}\sqsubseteq\neg\mathit{Univ},\mathit{Univ}\sqsubseteq\neg\mathit{NoExist},\mathit{NoExist}\sqsubseteq\neg\mathit{Exist} \}\\ &\cup\{ \mathit{NoExist}\sqsubseteq\neg\exists\mathit{Unsat}, \mathit{Exist}\sqsubseteq\neg\exists\mathit{Unsat} \} \end{align}\] \[\begin{align} \mathcal{A}=&\{\mathit{Unsat}(a,c_i)\mid 1\leq i\leq k\}\cup\{P(c_i,x_j)\mid x_j\in c_i\}\cup\{N(c_i,x_j)\mid \neg x_j\in c_i\}\\ &\cup\{P_\forall(c_i,x_j)\mid x_j\in c_i, j\leq n\}\cup\{N_\forall(c_i,x_j)\mid \neg x_j\in c_i, j\leq n\}\\ &\cup\{\mathit{Block}_\forall(a,x_j),\mathit{Block}_\exists(a,x_j),\mathit{Block}_\mathsf{all}(a,x_j)\mid 1\leq j\leq n+m\}\\ &\cup\{\mathit{NoExist}(a),\mathit{Exist}(a),\mathit{Univ}(a)\} \end{align}\] \[\begin{align} \mathit{NoExist}(a)&\succ\mathit{Exist}(a)\\ \mathit{Exist}(a)&\succ\mathit{Univ}(a)\\ \mathit{Block}_\mathsf{all}(a,x_j)&\succ\mathit{Block}_\forall(a,x_{j'})\\ \mathit{Block}_\forall(a,x_j)&\succ\mathit{Block}_\exists(a,x_{j'})\\ \mathit{Block}_Q(a,x_j)&\succ P(c_i,x_j) &Q\in\{\mathsf{all},\exists\}\\ \mathit{Block}_Q(a,x_j)&\succ N(c_i,x_j)&Q\in\{\mathsf{all},\exists\}\\ P(c_i,x_j)&\succ \mathit{Unsat}(a,c_i)\\ N(c_i,x_j)&\succ \mathit{Unsat}(a,c_i)\\ P(c_i,x_j)&\succ P_\forall(c_i,x_j)\\N(c_i,x_j)&\succ N_\forall(c_i,x_j) \end{align}\] Let \(\mathcal{A}'=\{\mathit{NoExist}(a)\}\cup\{\mathit{Block}_\mathsf{all}(a,x_j)\mid 1\leq j\leq n+m\}\). It is easy to check that \(\mathcal{A}'\in\mathit{GRep}(\mathcal{K}_\succ)\): \(\mathcal{A}'\) is a maximal \(\mathcal{T}\)-consistent subset of \(\mathcal{A}\) and there is no assertion preferred to \(\mathit{NoExist}(a)\) or \(\mathit{Block}_\mathsf{all}(a,x_j)\). We show that \(\Psi\) is valid iff \(|\mathit{GRep}(\mathcal{K}_\succ)|=1\), i.e., \(\mathcal{A}'\) is the unique globally-optimal repair.
(\(\Leftarrow\)) Assume that \(\Psi\) is not valid: there exists a valuation \(\nu_\forall\) of \(x_1,\dots,x_n\) such that for every valuation \(\nu\) of \(x_{1},\dots,x_{n+m}\) that extends \(\nu_\forall\), \(\nu(\Phi)\) evaluates to false. Let \[\begin{align} \mathcal{A}_\forall=& \{\mathit{Univ}(a)\}\cup\{\mathit{Block}_\exists(a,x_j)\mid 1\leq j\leq n+m\}\\& \cup\{P_\forall(c_i,x_j)\mid 1\leq j\leq n, x_j\in c_i, \nu_\forall(x_j)=\mathsf{true}\}\\& \cup\{N_\forall(c_i,x_j)\mid 1\leq j\leq n, \neg x_j\in c_i, \nu_\forall(x_j)=\mathsf{false}\} \\& \cup\{\mathit{Unsat}(a,c_i)\mid 1\leq i\leq k\}. \end{align}\] It is easy to check that \(\mathcal{A}_\forall\) is a repair. In particular, every \(x_j\) has only incoming \(P_\forall\) or \(N_\forall\) edges in \(\mathcal{A}_\forall\), so \(\mathcal{A}_\forall\) is \(\mathcal{T}\)-consistent. Moreover, it is not possible to add an assertion from \(\mathcal{A}\setminus\mathcal{A}_\forall\) while staying \(\mathcal{T}\)-consistent. In particular, the \(P\) and \(N\) assertions are in conflict with the \(\mathit{Block}_\exists\) assertions. We show that \(\mathcal{A}_\forall\in\mathit{GRep}(\mathcal{K}_\succ)\), which implies \(|\mathit{GRep}(\mathcal{K}_\succ)|\geq 2\).
Assume for a contradiction that there exists a global improvement \(\mathcal{A}''\) of \(\mathcal{A}_\forall\), i.e., a \(\mathcal{T}\)-consistent \(\mathcal{A}''\subseteq\mathcal{A}\), \(\mathcal{A}''\neq\mathcal{A}_\forall\), such that for every \(\alpha\in\mathcal{A}_\forall\setminus\mathcal{A}''\), there exists \(\beta\in\mathcal{A}''\setminus\mathcal{A}_\forall\) such that \(\beta\succ\alpha\). If \(\mathit{Exist}(a)\notin\mathcal{A}''\), then \(\mathcal{A}''\) contains \(\mathit{Univ}(a)\) by construction of \(\succ\). Hence \(\mathcal{A}''\) does not contain any \(\mathit{Block}_\forall(a,x_j)\), and by construction of \(\succ\) it follows that \(\mathcal{A}''\) contains all \(\mathit{Block}_\exists(a,x_j)\). Thus there is no \(P\) or \(N\) assertion in \(\mathcal{A}''\). Hence by construction of \(\succ\), \(\mathcal{A}''\) contains the same \(P_\forall\), \(N_\forall\), and \(\mathit{Unsat}\) assertions as \(\mathcal{A}_\forall\), so \(\mathcal{A}''=\mathcal{A}_\forall\), which contradicts our assumption on \(\mathcal{A}''\). It follows that \(\mathit{Exist}(a)\in\mathcal{A}''\). Hence \(\mathit{Unsat}(a,c_i)\notin\mathcal{A}''\) for every \(i\). By construction of \(\succ\), each \(c_i\) has thus an outgoing \(P\) or \(N\) edge in \(\mathcal{A}''\). It follows that \(\mathcal{A}''\) does not contain any \(P_\forall\) or \(N_\forall\) assertion. Hence, by construction of \(\succ\), for each \(P_\forall(c_i,x_j)\in\mathcal{A}_\forall\) (resp. \(N_\forall(c_i,x_j)\in\mathcal{A}_\forall\)), \(P(c_i,x_j)\in\mathcal{A}''\) (resp. \(N(c_i,x_j)\in\mathcal{A}''\)). Moreover, since \(\mathcal{A}''\) is \(\mathcal{T}\)-consistent, every \(x_j\) has only \(P\) or \(N\) incoming edges. Let \(\nu\) be the valuation of \(x_{1},\dots,x_{n+m}\) defined by \(\nu(x_j)=\mathsf{true}\) iff \(x_j\) has an incoming \(P\) edge in \(\mathcal{A}''\). It is easy to see that \(\nu\) satisfies all clauses of \(\Phi\) and that \(\nu\) extends \(\nu_\forall\). This contradicts our assumption on \(\nu_\forall\), so we conclude that \(\mathcal{A}_\forall\in\mathit{GRep}(\mathcal{K}_\succ)\).
(\(\Rightarrow\)) In the other direction, assume that \(\Psi\) is valid: for every valuation \(\nu_\forall\) of \(x_1,\dots,x_n\), there exists a valuation \(\nu\) of \(x_{1},\dots,x_{n+m}\) that extends \(\nu_\forall\) and such that \(\nu(\Phi)\) evaluates to true. Suppose for a contradiction that there is a globally-optimal repair \(\mathcal{A}''\neq\mathcal{A}'\). First note that every repair of \(\mathcal{A}\) contains either \(\mathit{Exist}(a)\), or \(\mathit{NoExist}(a)\), or \(\mathit{Univ}(a)\). Indeed, it is not possible to contradict these three assertions with a \(\mathcal{T}\)-consistent subset of \(\mathcal{A}\). We consider these three cases below.

If \(\mathit{Exist}(a)\in\mathcal{A}''\), then \(\mathit{NoExist}(a)\notin\mathcal{A}''\), \(\mathit{Univ}(a)\notin\mathcal{A}''\), and there is no \(\mathit{Block}_\exists\), \(\mathit{Block}_\mathsf{all}\) or \(\mathit{Unsat}\) assertions in \(\mathcal{A}''\). There is then no \(P_\forall\) or \(N_\forall\) assertions in \(\mathcal{A}''\): otherwise, \(\mathcal{A}''\setminus(\{P_\forall(c_i,x_j)\mid P_\forall(c_i,x_j)\in\mathcal{A}''\}\cup\{N_\forall(c_i,x_j)\mid N_\forall(c_i,x_j)\in\mathcal{A}''\})\cup\{P(c_i,x_j)\mid P_\forall(c_i,x_j)\in\mathcal{A}''\}\cup\{N(c_i,x_j)\mid N_\forall(c_i,x_j)\in\mathcal{A}''\}\) is a global improvement of \(\mathcal{A}''\). Hence, by maximality, \(\mathcal{A}''\) contains all \(\mathit{Block}_\forall\) assertions and a maximal \(\mathcal{T}\)-consistent subset of the \(P\) and \(N\) assertions. Hence, since \(\mathit{NoExist}(a)\succ\mathit{Exist}(a)\), \(\mathit{Block}_\mathsf{all}(a,x_j)\succ\mathit{Block}_\forall(a,x_{j'})\), \(\mathit{Block}_\mathsf{all}(a,x_j)\succ P(c_i,x_j)\) and \(\mathit{Block}_\mathsf{all}(a,x_j)\succ N(c_i,x_j)\), \(\mathcal{A}'\) is a global improvement of \(\mathcal{A}''\).

If \(\mathit{NoExist}(a)\in\mathcal{A}''\), then \(\mathit{Exist}(a)\notin\mathcal{A}''\), \(\mathit{Univ}(a)\notin\mathcal{A}''\), and there is no \(\mathit{Block}_\exists\), \(\mathit{Block}_\forall\) or \(\mathit{Unsat}\) assertions in \(\mathcal{A}''\). Moreover, there is no \(P_\forall\) or \(N_\forall\) assertions in \(\mathcal{A}''\) (otherwise, \(\mathcal{A}''\) can be improved by replacing the \(P_\forall\) or \(N_\forall\) assertions by the corresponding \(P\) or \(N\) assertions), and there is no \(P\) or \(N\) assertions in \(\mathcal{A}''\) (otherwise, \(\mathcal{A}''\) can be improved by replacing the \(P\) or \(N\) assertions by \(\mathit{Block}_\mathsf{all}\) assertions). It follows that \(\mathcal{A}''=\mathcal{A}'\) by maximality of repairs.

If \(\mathit{Univ}(a)\in\mathcal{A}''\), then \(\mathit{NoExist}(a)\notin\mathcal{A}''\), \(\mathit{Exist}(a)\notin\mathcal{A}''\), and there is no \(\mathit{Block}_\forall\) or \(\mathit{Block}_\mathsf{all}\) assertions in \(\mathcal{A}''\). Since \(\mathit{Block}_\exists(a,x_j)\succ P(c_i,x_j)\) and \(\mathit{Block}_\exists(a,x_j)\succ N(c_i,x_j)\), \(\mathcal{A}''\) does not contain any \(P\) or \(N\) assertions (otherwise \(\mathcal{A}''\) could be improved by replacing them by some \(\mathit{Block}_\exists\) assertions). Let \(\nu_\forall\) be the valuation of \(x_1,\dots,x_n\) such that \(\nu_\forall(x_j)=\mathsf{true}\) iff \(P_\forall(c_i,x_j)\in\mathcal{A}''\). Let \(\nu\) be a valuation that extends \(\nu_\forall\) and satisfies \(\Phi\). Consider \[\begin{align} \mathcal{A}_\nu=&\{\mathit{Exist}(a)\}\cup\{\mathit{Block}_\forall(a,x_j)\mid 1\leq j\leq n+m\} \\& \cup\{P(c_i,x_j)\mid x_j\in c_i, \nu(x_j)=\mathsf{true}\} \\&\cup\{N(c_i,x_j)\mid \neg x_j\in c_i, \nu(x_j)=\mathsf{false}\}. \end{align}\] We show that \(\mathcal{A}_\nu\) is a global improvement of \(\mathcal{A}''\). Indeed, (i) \(\mathit{Exist}(a)\succ\mathit{Univ}(a)\), (ii) \(\mathit{Block}_\forall(a,x_j)\succ\mathit{Block}_\exists(a,x_{j'})\), (iii) since \(\nu\) satisfies \(\Phi\) every \(c_i\) has an outgoing \(P\) or \(N\) edge in \(\mathcal{A}_\nu\) and \(P(c_i,x_j)\succ \mathit{Unsat}(a,c_i)\), \(N(c_i,x_j)\succ \mathit{Unsat}(a,c_i)\), and (iv) since \(\nu\) extends \(\nu_\forall\), for every \(P_\forall\) or \(N_\forall\) assertion in \(\mathcal{A}''\), the corresponding \(P\) or \(N\) assertion is in \(\mathcal{A}_\nu\) and \(P(c_i,x_j)\succ P_\forall(c_i,x_j)\), \(N(c_i,x_j)\succ N_\forall(c_i,x_j)\).

All cases lead to a contradiction, so there is no \(\mathcal{A}''\neq \mathcal{A}'\) such that \(\mathcal{A}''\in\mathit{GRep}(\mathcal{K}_\succ)\), i.e., \(|\mathit{GRep}(\mathcal{K}_\succ)|=1\). ◻

Proof. [21] have shown that when the priority relation is transitive, deciding uniqueness for globally-optimal repairs can be done in polynomial time when the conflict hypergraph is given. This result is applicable to all DLs with bounded conflicts, for which the conflict hypergraph is computable in polynomial time by checking the consistency of all subsets of size bounded by the maximal conflict size.

To show that the lower bounds of the other problems remain the same when \(\succ\) is transitive, some proofs have to be adapted.

Hardness of enumeration of globally-optimal repairs. The fact that enumeration of globally-optimal repairs is not in TotalP is not a corollary of the complexity of uniqueness as in the case where \(\succ\) is not transitive. We show that the associated decision problem of deciding whether a given set of ABox subsets is exactly \(\mathit{GRep}(\mathcal{K}_\succ)\) is coNP-hard. We show this by reduction from UNSAT. Let \(\Phi=c_1\wedge \dots\wedge c_k\) be a conjunction of clauses over variables \(x_1,\dots, x_m\). We define a KB \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\) and a transitive priority relation \(\succ\) over \(\mathcal{A}\) as follows.

\[\begin{align} \mathcal{T}=&\{\exists P^-\sqsubseteq\neg\exists N^-, \exists P\sqsubseteq\neg \exists\mathit{Unsat}^-, \exists N\sqsubseteq\neg \exists\mathit{Unsat}^-\}\\ &\cup\{\exists \mathit{Block}_Q^-\sqsubseteq\neg\exists P^-,\exists \mathit{Block}_ Q^-\sqsubseteq\neg\exists N^-,\mathit{Exist}\sqsubseteq\neg \exists \mathit{Block}_Q \mid Q\in\{\exists,\mathsf{all}\} \}\\ &\cup\{\exists \mathit{Block}_\exists\sqsubseteq\neg \exists \mathit{Block}_\mathsf{all}, \mathit{All}\sqsubseteq\neg\exists\mathit{Block}_\mathsf{all}, \mathit{Exist}\sqsubseteq\neg\mathit{All},\mathit{All}\sqsubseteq\neg\mathit{Sat}, \mathit{Sat}\sqsubseteq\neg\exists\mathit{Unsat} \}\\ \mathcal{A}=&\{\mathit{Unsat}(a,c_i)\mid 1\leq i\leq k\}\cup\{P(c_i,x_j)\mid x_j\in c_i\}\cup\{N(c_i,x_j)\mid \neg x_j\in c_i\}\\ &\cup\{\mathit{Block}_{\exists}(a,x_j),\mathit{Block}_{\mathsf{all}}(a,x_j)\mid 1\leq j\leq m\}\cup\{\mathit{Exist}(a),\mathit{Sat}(a),\mathit{All}(a)\} \end{align}\] \[\begin{align} \mathit{Sat}(a)&\succ\mathit{All}(a)\\ \mathit{Exist}(a)&\succ\mathit{Block}_{\exists}(a,x_j) \\ \mathit{Block}_{\mathsf{all}}(a,x_j) &\succ \mathit{Exist}(a)\\ \mathit{Block}_{\mathsf{all}}(a,x_j) &\succ \mathit{Block}_{\exists}(a, x_{j'})\\ \mathit{Block}_Q(a,x_j) &\succ P(c_i, x_j) &Q\in\{\mathsf{all},\exists\}\\ \mathit{Block}_Q(a,x_j) &\succ N(c_i, x_j)&Q\in\{\mathsf{all},\exists\}\\ P(c_i,x_j) &\succ \mathit{Unsat}(a,c_i)\\ N(c_i,x_j) &\succ \mathit{Unsat}(a,c_i) \end{align}\]

We show that \(\Phi\) is unsatisfiable iff \(\mathit{GRep}(\mathcal{K}_\succ)=\{\mathcal{A}_1,\mathcal{A}_2,\mathcal{A}_3\}\) where \[\begin{align} \mathcal{A}_1=&\{\mathit{Sat}(a)\}\cup\{\mathit{Block}_{\mathsf{all}}(a,x_j)\mid 1\leq j\leq m\},\\ \mathcal{A}_2=&\{\mathit{Block}_{\mathsf{all}}(a,x_j)\mid 1\leq j\leq m\}\cup\{\mathit{Unsat}(a,c_i)\mid 1\leq i\leq k\},\\ \mathcal{A}_3=&\{\mathit{All}(a)\}\cup\{\mathit{Block}_{\exists}(a,x_j)\mid 1\leq j\leq m\}\cup\{\mathit{Unsat}(a,c_i)\mid 1\leq i\leq k\}. \end{align}\] (\(\Leftarrow\)) Assume that \(\Phi\) is satisfiable. Then \(\mathcal{A}_3\notin\mathit{GRep}(\mathcal{K}_\succ)\). Indeed, let \(\nu\) be a valuation that satisfies \(\Phi\) and \[\begin{align} \mathcal{A}_\nu=&\{\mathit{Sat}(a),\mathit{Exist}(a)\}\cup\{P(c_i,x_j)\mid P(c_i,x_j)\in\mathcal{A},\nu(x_j)=\mathsf{true}\}\cup\{N(c_i,x_j)\mid N(c_i,x_j)\in\mathcal{A},\nu(x_j)=\mathsf{false}\}. \end{align}\] Since \(\mathit{Sat}(a)\succ\mathit{All}(a)\), \(\mathit{Exist}(a)\succ\mathit{Block}_{\exists}(a,x_j)\), \(P(c_i,x_j)\succ\mathit{Unsat}(a,c_i)\), \(N(c_i,x_j)\succ\mathit{Unsat}(a,c_i)\), and each \(c_i\) has a \(P\) or \(N\) outgoing edge in \(\mathcal{A}_\nu\) because \(\nu\) satisfies \(\Phi\), \(\mathcal{A}_\nu\) is a global improvement of \(\mathcal{A}_3\). It follows that \(\mathit{GRep}(\mathcal{K}_\succ)\neq\{\mathcal{A}_1,\mathcal{A}_2,\mathcal{A}_3\}\).
(\(\Rightarrow\)) Assume that \(\Phi\) is unsatisfiable. We first show that \(\{\mathcal{A}_1,\mathcal{A}_2,\mathcal{A}_3\}\subseteq \mathit{GRep}(\mathcal{K}_\succ)\). It is easy to check that \(\mathcal{A}_1,\mathcal{A}_2,\mathcal{A}_3\) are repairs of \(\mathcal{K}_\succ\). We show that they are globally-optimal repairs.

\(\mathcal{A}_1\in\mathit{GRep}(\mathcal{K}_\succ)\) because none of its assertions is dominated by any other.
\(\mathcal{A}_2\in\mathit{GRep}(\mathcal{K}_\succ)\) because its \(\mathit{Block}_{\mathsf{all}}\) assertions are not dominated by any others and the only assertions of greater priority than the \(\mathit{Unsat}\) assertions are the \(P\), \(N\) which are in conflict with the \(\mathit{Block}_{\mathsf{all}}\) assertions.
For \(\mathcal{A}_3\), assume for a contradiction that there exists a \(\mathcal{T}\)-consistent \(\mathcal{A}''\subseteq\mathcal{A}\), \(\mathcal{A}''\neq\mathcal{A}_3\) such that for every \(\alpha\in\mathcal{A}_3\setminus\mathcal{A}''\), there exists \(\beta\in\mathcal{A}''\setminus\mathcal{A}_3\) such that \(\beta\succ\alpha\). First note that since \(\Phi\) is unsatisfiable, it is not possible that \(\mathcal{A}''\) contains a \(\mathcal{T}\)-consistent set of \(P\) and \(N\) assertions such that every \(c_i\) has an outgoing \(P\) or \(N\) edge in \(\mathcal{A}''\). By construction of \(\succ\), it thus follows that \(\mathcal{A}''\) contains at least one \(\mathit{Unsat}\) assertion. If \(\mathit{All}(a)\notin \mathcal{A}''\), then by construction of \(\succ\), \(\mathit{Sat}(a)\in \mathcal{A}''\), which contradicts the \(\mathcal{T}\)-consistency of \(\mathcal{A}''\) since \(\mathit{Sat}\sqsubseteq \neg \exists\mathit{Unsat}\in\mathcal{T}\). It follows that \(\mathit{All}(a)\in \mathcal{A}''\). By \(\mathcal{T}\)-consistency of \(\mathcal{A}''\), \(\mathit{Exist}(a)\) and the \(\mathit{Block}_{\mathsf{all}}\) assertions are thus not in \(\mathcal{A}''\). Since they are the only assertions dominating the \(\mathit{Block}_\exists\) assertions, it follows that \(\mathit{Block}_\exists\) assertions are in \(\mathcal{A}'\), so that there is no \(P\) or \(N\) assertions in \(\mathcal{A}'\), and \(\mathcal{A}''=\mathcal{A}_3\).

We now show that \(\mathit{GRep}(\mathcal{K}_\succ)\subseteq\{\mathcal{A}_1,\mathcal{A}_2,\mathcal{A}_3\}\). Let \(\mathcal{A}'\in\mathit{GRep}(\mathcal{K}_\succ)\).

Assume that \(\mathit{Sat}(a)\in\mathcal{A}'\). Then \(\mathcal{A}'\) does not contain \(\mathit{All}(a)\), or any \(\mathit{Unsat}(a,c_i)\). Assume for a contradiction that \(\mathcal{A}'\neq\mathcal{A}_1\). Since \(\mathit{Block}_{\mathsf{all}}(a,x_j) \succ P(c_i, x_j)\), \(\mathit{Block}_{\mathsf{all}}(a,x_j) \succ N(c_i, x_j)\), \(\mathit{Block}_{\mathsf{all}}(a,x_j) \succ \mathit{Block}_\exists(a,x_{j'})\), and \(\mathit{Block}_{\mathsf{all}}(a,x_j) \succ \mathit{Exist}(a)\), then \(\mathcal{A}_1\) is a global improvement of \(\mathcal{A}'\). It follows that \(\mathcal{A}'=\mathcal{A}_1\).
Assume that \(\mathit{All}(a)\in\mathcal{A}'\). Then \(\mathcal{A}'\) does not contain \(\mathit{Exist}(a)\), \(\mathit{Sat}(a)\), or any \(\mathit{Block}_{\mathsf{all}}(a, x_j)\). Assume for a contradiction that \(\mathcal{A}'\neq\mathcal{A}_3\). If \(\mathcal{A}'\subseteq\mathcal{A}_3\), it is clear that \(\mathcal{A}'\) is not a repair, so \(\mathcal{A}'\not\subseteq\mathcal{A}_3\). Thus \(\mathcal{A}'\) must contain some \(P\) or \(N\) assertions. But in this case we obtain a global improvement of \(\mathcal{A}'\) by replacing the \(P\) and \(N\) assertions by the conflicting \(\mathit{Block}_{\exists}\) assertions.
In the case where \(\mathit{All}(a)\notin\mathcal{A}'\) and \(\mathit{Sat}(a)\notin\mathcal{A}'\), we show that \(\mathcal{A}'=\mathcal{A}_2\). First note that since \(\mathit{All}(a)\notin\mathcal{A}'\) and the \(\mathit{Block}_{\mathsf{all}}\) assertions are of greater priority than any other assertions they are in conflict with, \(\mathcal{A}'\) contains all the \(\mathit{Block}_{\mathsf{all}}\) assertions. By \(\mathcal{T}\)-consistency and maximality of \(\mathcal{A}'\), it follows that \(\mathcal{A}'=\mathcal{A}_2\).

We have thus shown that \(\mathit{GRep}(\mathcal{K}_\succ)=\{\mathcal{A}_1,\mathcal{A}_2,\mathcal{A}_3\}\).

Hardness of uniqueness and enumeration for Pareto-optimal repairs. We adapt the reduction given in the proof of Theorem [ThmUniqueness]: since in this reduction, imposing transitivity on \(\succ\) would lead to \(\mathit{Unsat}(a,c_i)\succ P(c_i,x_j)\) and \(\mathit{Unsat}(a,c_i)\succ N(c_i,x_j)\), we prevent this by creating two versions (identified by indexes 1 and 2) of all concepts and roles and letting \(\mathit{Unsat}_1\) in conflict with \(P_2\), \(N_2\) instead of \(P_1\), \(N_1\), and similarly for \(\mathit{Unsat}_2\). Given a conjunction of clauses \(\Phi=c_1\wedge \dots\wedge c_k\) over variables \(x_1,\dots, x_n\), we construct \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\) and \(\succ\) as follows. \[\begin{align} \mathcal{T}=&\{\exists P_l^-\sqsubseteq\neg\exists N_l^-,\exists\mathit{Block}_l^-\sqsubseteq\neg \exists P_l^-, \exists\mathit{Block}_l^-\sqsubseteq\neg \exists N_l^- \mid l\in\{1,2\}\}\\ &\cup\{ \exists P_l\sqsubseteq\neg \exists\mathit{Unsat}_r^-, \exists N_l\sqsubseteq\neg \exists\mathit{Unsat}_r^-\mid (l,r)\in\{(1,2),(2,1)\}\} \\ &\cup\{ \mathit{Exist}_l\sqsubseteq\neg\exists\mathit{Block}_l, \mathit{Exist}_l\sqsubseteq\neg\exists\mathit{Unsat}_l, \mathit{Exist}_l\sqsubseteq\neg\mathit{NoExist}_l \mid l\in\{1,2\}\}\\ \mathcal{A}=&\{\mathit{Unsat}_l(a,c_i)\mid 1\leq i\leq k, l\in\{1,2\}\}\cup\{P_l(c_i,x_j)\mid x_j\in c_i, l\in\{1,2\}\}\cup\{N_l(c_i,x_j)\mid \neg x_j\in c_i, l\in\{1,2\}\} \\ &\cup\{\mathit{Block}_l(a,x_j)\mid 1\leq j\leq n, l\in\{1,2\}\} \cup\{\mathit{Exist}_l(a),\mathit{NoExist}_l(a)\mid l\in\{1,2\} \} \end{align}\] \[\begin{align} \mathit{Unsat}_l(a,c_i)\succ& \mathit{Exist}_l(a) & \,l\in\{1,2\}\\ \mathit{Exist}_l(a)\succ&\mathit{Block}_l(a,x_j) & l\in\{1,2\}\\ \mathit{Block}_l(a,x_j)\succ& P_l(c_i,x_j) &l\in\{1,2\}\\ \mathit{Block}_l(a,x_j)\succ& N_l(c_i,x_j) &l\in\{1,2\} \end{align}\] Note that \(\succ\) is transitive (in particular, because the \(\mathit{Unsat}_1\) assertions are in conflict with the \(P_2\) and \(N_2\) assertions but not with the \(P_1\) and \(N_1\), and vice versa). Let \[\mathcal{A}'=\{\mathit{NoExist}_1(a), \mathit{NoExist}_2(a)\}\cup\{\mathit{Block}_1(a,x_j), \mathit{Block}_2(a,x_j)\mid 1\leq j\leq n\}\cup\{\mathit{Unsat}_1(a,c_i), \mathit{Unsat}_2(a,c_i)\mid 1\leq i\leq k\}.\] It is easy to check that \(\mathcal{A}'\in\mathit{PRep}(\mathcal{K}_\succ)\): \(\mathcal{A}'\) is \(\mathcal{T}\)-consistent, and it is not possible to add any assertion \(\alpha\in\mathcal{A}\setminus\mathcal{A}'\) to \(\mathcal{A}'\) while staying \(\mathcal{T}\)-consistent without removing an assertion \(\beta\in\mathcal{A}'\) such that \(\alpha\not\succ\beta\). We show that \(\Phi\) is unsatisfiable iff \(\mathcal{A}'\) is the unique Pareto-optimal repair.
(\(\Leftarrow\)) Assume that \(\Phi\) is satisfiable: there exists a valuation \(\nu\) that satisfies \(\Phi\). Let \(\mathcal{A}_\nu=\{P_1(c_i,x_j), P_2(c_i,x_j)\mid x_j\in c_i, \nu(x_j)=\mathsf{true}\}\cup\{N_1(c_i,x_j), N_2(c_i,x_j)\mid \neg x_j\in c_i, \nu(x_j)=\mathsf{false}\} \cup\{\mathit{Exist}_1(a), \mathit{Exist}_2(a)\}\). Using arguments similar to those used in the case where \(\succ\) was not transitive, we can show that \(\mathcal{A}_\nu\in\mathit{PRep}(\mathcal{K}_\succ)\), so that \(|\mathit{PRep}(\mathcal{K}_\succ)|\geq 2\).
(\(\Rightarrow\)) In the other direction, assume that there exists a Pareto-optimal repair \(\mathcal{A}''\neq\mathcal{A}'\). First we show that for \(l\in\{1,2\}\), if \(\mathit{Exist}_l(a)\notin\mathcal{A}''\), then \(\mathcal{A}''\) contains \(\mathit{NoExist}_l(a)\) and all \(\mathit{Block}_l\) and \(\mathit{Unsat}_l\) assertions, but no \(P_l\) or \(N_l\) assertions. Indeed, if \(\mathit{Exist}_l(a)\notin\mathcal{A}''\), by maximality, \(\mathit{NoExist}_l(a)\in\mathcal{A}''\). Moreover, if \(\mathcal{A}''\) contains some \(P_l\) or \(N_l\) assertions, then all \(P_l\) or \(N_l\) edges incoming in some \(x_j\) can be replaced by \(\mathit{Block}_l(a,x_j)\) to obtain a Pareto improvement of \(\mathcal{A}''\) and \(\mathcal{A}''\notin\mathit{PRep}(\mathcal{K}_\succ)\). Thus \(\mathcal{A}''\) contains no \(P_l\) or \(N_l\) assertions. By maximality, it thus contains all \(\mathit{Block}_l\) and \(\mathit{Unsat}_l\) assertions.

Thus if \(\mathit{Exist}_1(a)\notin\mathcal{A}''\) and \(\mathit{Exist}_2(a)\notin\mathcal{A}''\), then \(\mathcal{A}''=\mathcal{A}'\). It follows that \(\mathit{Exist}_l(a)\in\mathcal{A}''\) for \(l=1\) or \(l=2\). Assume w.l.o.g. that \(\mathit{Exist}_1(a)\in\mathcal{A}''\). Assume for a contradiction that \(\mathit{Exist}_2(a)\notin\mathcal{A}''\). It follows from the preceding paragraph that \(\mathcal{A}''\) contains no \(P_2\) or \(N_2\) assertions. Thus \(\mathit{Exist}_1(a)\) can be replaced by the \(\mathit{Unsat}_1\) assertions to obtain a Pareto improvement of \(\mathcal{A}''\) and \(\mathcal{A}''\notin\mathit{PRep}(\mathcal{K}_\succ)\). It follows that for \(l\in\{1,2\}\), \(\mathit{Exist}_l(a)\in\mathcal{A}''\). Hence \(\mathit{NoExist}_l(a)\notin\mathcal{A}''\) and there is no \(\mathit{Block}_l\) or \(\mathit{Unsat}_l\) assertions in \(\mathcal{A}''\). Thus the remaining assertions of \(\mathcal{A}''\) form a maximal subset of the \(P_1\), \(N_1\) and \(P_2\), \(N_2\) assertions such that no \(x_j\) has both \(P_l\) and \(N_l\) incoming edges for \(l\in\{1,2\}\). The valuation of the \(x_j\) defined by \(\nu(x_j)=\mathsf{true}\) iff \(x_j\) has an incomming \(P_1\) edge in \(\mathcal{A}''\) satisfies \(\Phi\). Otherwise, there would be a \(c_i\) without \(P_1\) or \(N_1\) outgoing edge and it would be possible to add \(\mathit{Unsat}_2(a,c_i)\) and remove \(\mathit{Exist}_2(a)\) to improve \(\mathcal{A}''\) since \(\mathit{Unsat}_2(a,c_i)\succ \mathit{Exist}_2(a)\). It follows that \(\Phi\) is satisfiable.

Hardness of P-AR, P-IAR, P-brave, C-AR, C-IAR, C-brave IQ entailment. For Pareto-optimal and completion-optimal repairs, coNP-hardness (resp. NP-hardness) of AR and IAR (resp. brave) IQ entailment in DL-Lite\(_{\mathsf{core}}\) follow from the case where the priority relation is given by priority levels, in which the three families of optimal repairs coincide [17], [29]. These results apply since when \(\succ\) is given by priority levels, \(\succ\) is transitive: if \(\alpha_1\succ\dots\succ\alpha_n\), then \(s(\alpha_1)>\dots>s(\alpha_n)\), so if \(\{\alpha_1,\alpha_n\}\subseteq C\in\mathit{Conf}(\mathcal{K})\), then \(\alpha_1\succ\alpha_n\).

Hardness of G-AR, G-IAR, G-brave IQ entailment. The reduction used in the proof Theorem [ThmHardnessGlobal] is such that \(\succ\) is transitive.

Hardness of globally-optimal repair checking. We use the reduction given for the lower bound of globally-optimal repairs enumeration: we have shown that \(\mathcal{A}_3\in\mathit{GRep}(\mathcal{K}_\succ)\) iff \(\Phi\) is unsatisfiable. ◻

10 Proofs for Section 5 ↩︎

Proof. Let \(P=(\mathit{Args},\rightsquigarrow, \succ)\) be a symmetric PAF. Take some preferred extension \(E\) of \(P\). Then \(E\) is a preferred extension of the corresponding AF \(F=(\mathit{Args}, \rightsquigarrow_\succ)\). Suppose for a contradiction that \(E\) is not a stable extension of the PAF \(P\), which means \(E\) is not a stable extension of \(F\), i.e., \(E^+\neq\mathit{Args}\setminus E\). Since \(E\) is conflict-free, it must then be the case that there is some \(\beta \in \mathit{Args}\setminus E\) such that \(\beta \not \in E^+\). Because \(\succ\) is acyclic, we can w.l.o.g. choose \(\beta\) such that there is no \(\beta' \in (\mathit{Args}\setminus E) \setminus E^+\) with \(\beta' \succ \beta\). Since \(E\) is a preferred extension, \(E \cup \{\beta\}\) cannot be admissible in \(F\), and since \(E \cup \{\beta\}\) is conflict-free, it follows that there is an undefended attack on \(E \cup \{\beta\}\). Since \(E\) defends itself, the attack must be on \(\beta\), i.e., \(\beta \not \in \Gamma_{F}(E \cup \{\beta\})\). We can thus find an attack \(\gamma \rightsquigarrow_\succ\beta\) such that \(\gamma \not \in E \cup \{\beta\}\) and \(\gamma \not \in (E \cup \{\beta\})^+\). In particular, \(\beta \not \rightsquigarrow_\succ\gamma\). As \(P\) is a symmetric PAF, we know that \(\beta \rightsquigarrow\gamma\), and since \(\beta \not \rightsquigarrow_\succ\gamma\), it must be the case that \(\gamma \succ \beta\). But we now have \(\gamma \in (\mathit{Args}\setminus E) \setminus E^+\) and \(\gamma \succ \beta\), which contradicts our choice of \(\beta\), concluding our argument. ◻

Proof. Let \(F=(\mathit{Args}, \rightsquigarrow_\succ)\) be the corresponding AF of a symmetric PAF \(P=(\mathit{Args},\rightsquigarrow, \succ)\), and assume that \(\alpha_1 \rightsquigarrow_\succ \alpha_2\rightsquigarrow_\succ \dots\rightsquigarrow_\succ \alpha_n\rightsquigarrow_\succ \alpha_1\). Since \(F\) is the corresponding AF of \(P\), then \(\alpha_1 \rightsquigarrow\alpha_2\rightsquigarrow\dots\rightsquigarrow\alpha_n\rightsquigarrow\alpha_1\). Moreover, since \(P\) is symmetric, \((\mathit{Args},\rightsquigarrow)\) is symmetric, and it follows that \(\alpha_2\rightsquigarrow\alpha_1\), ..., \(\alpha_n \rightsquigarrow\alpha_{n-1}\), and \(\alpha_1\rightsquigarrow\alpha_n\) Finally, since \(\succ\) is acyclic, there must exist \((j,i)\in\{(1,2),\dots,(n-1,n),(n,1)\}\) such that \(\alpha_j\not\succ\alpha_i\), which implies that \(\alpha_i\rightsquigarrow_\succ\alpha_j\).

In the other direction, let \(F=(\mathit{Args}, \rightsquigarrow)\) be an AF such that for any cycle \(\alpha_1 \rightsquigarrow\alpha_2\rightsquigarrow\dots\rightsquigarrow\alpha_n\rightsquigarrow\alpha_1\), there exists \((j,i)\in\{(1,2),\dots,(n-1,n),(n,1)\}\) with \(\alpha_i\rightsquigarrow\alpha_j\). Define \(P=(\mathit{Args},\rightsquigarrow^P, \succ)\) by \(\rightsquigarrow^P=\{(\alpha,\beta)\mid \alpha\rightsquigarrow\beta\}\cup\{(\alpha,\beta)\mid \beta\rightsquigarrow\alpha\}\) and \(\alpha\succ\beta\) iff \(\alpha\rightsquigarrow\beta\) and \(\beta\not\rightsquigarrow\alpha\). We first show that \(\succ\) is acyclic. If it was not the case, there would be a cycle \(\alpha_1 \succ \alpha_2 \succ \dots \succ \alpha_n \succ \alpha_1\). By construction of \(\succ\), it would then be the case that \(\alpha_1 \rightsquigarrow\alpha_2\rightsquigarrow\dots\rightsquigarrow\alpha_n\rightsquigarrow\alpha_1\) and for every \((j,i)\in\{(1,2),\dots,(n-1,n),(n,1)\}\), \(\alpha_i\not\rightsquigarrow\alpha_j\), a contradiction. It is then easy to verify that \(F\) is the corresponding AF of \(P\):

if \(\alpha \rightsquigarrow\beta\) then \(\alpha \rightsquigarrow^P \beta\) by construction of \(\rightsquigarrow^P\) and \(\beta \not \succ \alpha\) otherwise \(\alpha\not\rightsquigarrow\beta\) by construction of \(\succ\);
if (i) \(\alpha \rightsquigarrow^P \beta\) and (ii) \(\beta \not \succ \alpha\), then it follows from (i) that \(\alpha \rightsquigarrow\beta\) or \(\beta\rightsquigarrow\alpha\), and from (ii) that \(\beta\not\rightsquigarrow\alpha\) or \(\alpha\rightsquigarrow\beta\), so \(\alpha\rightsquigarrow\beta\).

◻

Proof. Let \(F=(\mathit{Args},\rightsquigarrow)\) be a strongly symmetric SETAF. Suppose for a contradiction that there is a preferred extension \(E\) that is not a stable extension. Then \((\mathit{Args}\setminus E) \setminus E^+ \neq \emptyset\). Let \(B=\{\beta_1, \ldots, \beta_n\}\) be a \(\subseteq\)-maximal subset of \((\mathit{Args}\setminus E) \setminus E^+\) that is conflict-free. We show with the following two claims that \(E \cup B\) is admissible, which contradicts the fact that \(E\) is a preferred extension, and therefore allows us to conclude that \(E\) is stable.
Claim: \(E \cup B\) is conflict-free.
Proof of claim. Suppose that \(E \cup B\) is not conflict-free. As \(E\) is conflict-free and \(B\) is conflict-free, any attack contained in \(E \cup B\) must contain elements from both \(E\) and \(B\). Moreover, since \(F\) is strongly symmetric, we may assume that the attack targets an element of \(E\). Thus, there exists \(S \subseteq E \cup B\) with \(S \cap B \neq \emptyset\) and \(\varepsilon \in E\) such that \(S \rightsquigarrow\varepsilon\). Since \(E\) is a preferred extension, we must have \((S \setminus E) \cap E^+ \neq \emptyset\), which implies \(B \cap E^+ \neq \emptyset\). This is a contradiction, since \(B \subseteq \mathit{Args}\setminus E^+\).
Claim: \(E \cup B \subseteq \Gamma_{F}(E \cup B)\).
Proof of claim. Suppose for a contradiction that \(E \cup B \not \subseteq \Gamma_{F}(E \cup B)\). Then there exists an attack \(S \rightsquigarrow\alpha\) such that \(\alpha \in E \cup B\) and \(S \cap (E \cup B)^+ = \emptyset\). Since \(E\) is a preferred extension, we know that \(E \subseteq \Gamma_{F}(E) \subseteq \Gamma_{F}(E \cup B)\), so \(\alpha \in B\). Since \(E \cup B\) is conflict-free (by the preceding claim), there must exist \(\sigma \in S \setminus (E \cup B)\). As \(S \cap (E \cup B)^+ = \emptyset\), we must have \(\sigma \in (\mathit{Args}\setminus E) \setminus E^+\). From the maximality of \(B\), we know that \(B \cup \{\sigma\}\) is not conflict-free, and since \(B\) is conflict-free, there must be an attack that involves \(\sigma\). Moreover, as \(F\) is strongly symmetric, we can assume that \(\sigma\) is the target of the attack, which yields \(\sigma \in B^+\), again contradicting \(S \cap (E \cup B)^+ = \emptyset\). ◻

Proof. Let \(P=(\mathit{Args}, \rightsquigarrow, \succ)\) be a strongly symmetric PSETAF such that \(\succ\) is transitive, and let \(F=(\mathit{Args}, \rightsquigarrow_\succ)\) be the corresponding SETAF. Suppose for a contradiction that \(S_0\) is a preferred extension of \(P\) but not a stable extension of \(P\). It follows that \(S_0\) is a preferred extension of \(F\) but not a stable extension of \(F\). To obtain a contradiction, we will construct an admissible set which is a proper superset of \(S_0\). To initiate the construction, we will require the following claim.
Claim 1. There exists \(\alpha \in (\mathit{Args}\setminus S_0)\) such that \(S_0 \cup \{\alpha\}\) is conflict-free in \(F\).
Proof of claim. Since \(S_0\) is preferred but not stable, there is \(\alpha \in (\mathit{Args}\setminus S_0)\) such that \(\alpha \not \in S_0^+\). Suppose for a contradiction that \(S_0 \cup \{\alpha\}\) is not conflict-free. As \(\alpha \not \in S_0^+\), it follows that there is some \(S' \subseteq S_0\) and \(\sigma \in S_0\) such that \(S' \cup \{\alpha\} \rightsquigarrow_\succ\sigma\). However, since \(S_0\) is preferred, it must defend itself against this attack, and since \(S_0\) is conflict-free, the only possibility is that \(\alpha \in S_0^+\), which yields a contradiction. (end proof of claim)
We now proceed to construct a finite sequence \(S_0, S_1, S_2, \ldots, S_n\) of subsets of \(\mathit{Args}\) as follows:

While there exists \(\alpha\) such that (i) \(\alpha \in (\mathit{Args}\setminus S_i)\) and (ii) \(S_i \cup \{\alpha\}\) is conflict-free
- Pick some \(\alpha_i\) that satisfies (i) and (ii) and such that there is no \(\alpha_i'\) satisfying (i) and (ii) with \(\alpha_i' \succ \alpha_i\) (such an \(\alpha_i\) must exist due to the acyclicity of \(\succ\)).
- Set \(S_{i+1} = S_i \cup \{\alpha_i\}\)

Since for every \(i \geq 0\), we have \(S_i \subseteq \mathit{Args}\) and \(S_i \subsetneq S_{i+1}\), the construction will terminate after a finite number of iterations. We observe that each \(S_i\) is conflict-free. We will show that the final set \(S_n\) is conflict-free and defends itself against all attacks, which contradicts the fact that \(S_0\) is a preferred extension. The main ingredient in showing this is the following claim:
Claim 2. For each \(0 \leq i \leq n\), the following property holds:

For each attack \(T \rightsquigarrow_\succ\sigma\) on \(S_i\) such that \(T \cap S_i^+ = \emptyset\) (i.e.\(S_i\) does not defend against this attack):

(a)

if \(i \geq 1\) and \(\tau \in T \setminus S_{i}\), then the set \(S_{i-1} \cup \{\tau\}\) is conflict-free;

(b)

for every \(\tau \in T\setminus S_i\), \(\tau \not \succ \sigma'\) for all \(\sigma' \in S_i \setminus S_0\);

(c)

there exists \(\tau \in T\setminus S_i\) such that \(\tau \not \succ \tau'\) for every \(\tau' \in T \cup \{\sigma\} \setminus \{\tau\}\).

Proof of claim. The base case (\(i=0\)) is trivial, as \(S_0\) is a preferred extension, and so there is no undefended attack. We will suppose that we have already shown the property to hold for \(i=0, \ldots, k\) and prove it still holds for \(i=k+1\). Let us consider some attack \(T \rightsquigarrow_\succ\sigma\) with \(\sigma \in S_{k+1}\) such that \(T \cap S_{k+1}^+ = \emptyset\). We need to show that conditions (a), (b), and (c) are satisfied. We prove each condition in turn.
Claim 2.1: Condition (a) holds: for every \(\tau \in T \setminus S_{k+1}\), the set \(S_k \cup \{\tau\}\) is conflict-free.
Proof of claim. Suppose for a contradiction that \(S_k \cup \{\tau\}\) is not conflict-free. The attack contained in \(S_k \cup \{\tau\}\) cannot target \(\tau\), since otherwise we would have \(\tau \in T \cap S_k^+\), contradicting the fact that \(T\cap S_{k+1}^+=\emptyset\). The conflict must however involve \(\tau\) since \(S_{k}\) is conflict-free. Thus, there must exist \(S^* \subseteq S_k\) and \(\sigma^* \in S_k\) such that \(S^* \cup \{\tau\} \rightsquigarrow_\succ\sigma^*\). If \((S^* \cup \{\tau\})\cap S_{k+1}^+ \neq \emptyset\), then we must have \(\tau \in S_{k+1}^+\), which again gives a contradiction. Thus, \((S^* \cup \{\tau\})\cap S_{k+1}^+ = \emptyset\), which implies \((S^* \cup \{\tau\})\cap S_{k}^+ = \emptyset\). We can therefore apply the induction hypothesis for \(i=k\). As \((S^* \cup \{\tau\}) \setminus S_k = \{\tau\}\), it follows from condition (c) applied to the undefended attack \(S^* \cup \{\tau\} \rightsquigarrow_\succ\sigma^*\) that \(\tau \not \succ \beta\) for all \(\beta \in S^* \cup \{\sigma^*\}\). Since \(P\) is strongly symmetric, it follows that we also have the attack \(S^* \cup \{\sigma^*\} \rightsquigarrow_\succ\tau\). But this means that \(T \cap S_k^+ \neq \emptyset\), so \(T \cap S_{k+1}^+ \neq \emptyset\), a contradiction. (end proof of claim)
Claim 2.2: Condition (b) holds: for every \(\tau \in T\setminus S_{k+1}\), \(\tau \not \succ \sigma'\) for all \(\sigma' \in S_{k+1} \setminus S_0\).
Proof of claim. Suppose for a contradiction that the condition does not hold. Since \(S_{k+1} \setminus S_0= \{\alpha_0, \ldots, \alpha_{k-1}, \alpha_{k}\}\), this means that there exists \(\tau \in T\setminus S_{k+1}\) and \(0 \leq j \leq k\) such that \(\tau \succ \alpha_j\). Since \(\alpha_j\) was selected for addition to \(S_j\) despite \(\tau \succ \alpha_j\), it must be the case that \(S_j \cup \{\tau\}\) is not conflict-free. As \(S_j \subseteq S_k\), the set \(S_k \cup \{\tau\}\) must also contain some attack, which contradicts Claim 2.1, which states that \(S_k \cup \{\tau\}\) is conflict-free. (end proof of claim)
Claim 2.3: Condition (c) holds: there exists \(\tau \in T\setminus S_{k+1}\) such that \(\tau \not \succ \tau'\) for every \(\tau' \in T \cup \{\sigma\} \setminus \{\tau\}\).
Proof of claim. Suppose for a contradiction that condition (c) does not hold. Then for every \(\tau \in T\setminus S_{k+1}\), there exists \(\tau' \in (T \cup \{\sigma\} \setminus \{\tau\})\) such that \(\tau \succ \tau'\). However, due to Claim 2.2, we know that \(\tau' \not \in S_{k+1} \setminus S_0\). Moreover, we also know that \(\sigma \in S_{k+1} \setminus S_0\), since \(T \cap S_{k+1}^+ = \emptyset\), while every attack on \(S_0\) is defended (\(S_0\) being a preferred extension). Thus, we have: \[\label{prop1} \text{For every \tau \in T\setminus S_{k+1}, there exists \tau' \in (T \setminus (S_{k+1} \setminus S_0)) \setminus \{\tau\} such that \tau \succ \tau'.}\tag{1}\] Define \(S_0^*\) as the restriction of \(S_0\) to those elements \(s_0 \in S_0\) such that \(s_0 \not \succ \tau'\) for every \(\tau' \in S_{k+1} \setminus S_0\). We aim to show that if \(\tau \in T\setminus S_{k+1}\) and \(s_0 \in S_0 \setminus S_0^*\), then \(\tau \not \succ s_0\). Suppose for a contradiction that we have \(\tau \succ s_0\) for such a \(\tau\) and \(s_0\). From \(s_0 \in S_0 \setminus S_0^*\), we know that there exists \(\tau' \in S_{k+1} \setminus S_0\) such that \(s_0 \succ \tau'\). But then by transitivity of \(\succ\), we must also have \(\tau \succ \tau'\), which contradicts Claim 2.2. We can thus refine the preceding statement as follows: \[\label{prop2} \text{For every \tau \in T\setminus S_{k+1}, there exists \tau' \in (T \setminus (S_{k+1}\cup \{\tau\})) \cup (T \cap S_0^*) such that \tau \succ \tau'.}\tag{2}\] Next consider \(\sigma_0 \in T \cap S_0^*\), and suppose for a contradiction that there is no \(\tau' \in T \cup \{\sigma\}\) such that \(\sigma_0 \succ \tau'\). Since \(P\) is strongly symmetric and \(T \rightsquigarrow_\succ\sigma\), we must have \(T \setminus \{\sigma_0\} \cup \{\sigma\} \rightsquigarrow_\succ\sigma_0\). We know that \((T \setminus \{\sigma_0\} \cup \{\sigma\}) \cap S_0^+ \neq \emptyset\) since \(S_0\) is a preferred extension of \(F\). As \(\sigma \in S_{k+1}\) and \(S_{k+1}\) is conflict-free, it must be the case that \((T \setminus S_{k+1}) \cap S_0^+ \neq \emptyset\). But this means that \(T \cap S_{k+1}^+ \neq \emptyset\), a contradiction. When combined with the definition of \(S_0^*\) and the transitivity of \(\succ\), we get: \[\label{prop3} \text{For every \sigma_0 \in T \cap S_0^*, there exists \tau' \in T \setminus (S_{k+1} \setminus S_0^*) such that \sigma_0 \succ \tau'.}\tag{3}\] Since \(S_{k+1}\) is conflict-free, we know that \(T\setminus S_{k+1} \neq \emptyset\). This means that the set \((T \setminus S_{k+1}) \cup (T \cap S_0^*)\) is non-empty. Moreover, statements (2 ) and (3 ) show that for every \(\tau \in (T \setminus S_{k+1}) \cup (T \cap S_0^*)\) there exists \(\tau' \in (T \setminus S_{k+1}) \cup (T \cap S_0^*)\) such that \(\tau \succ \tau'\). This implies the existence of a cycle in the preference relation \(\succ\), contradicting the fact that \(\succ\) is acyclic. (end proof of claim)
We have thus established Claim 2. Now consider the final set \(S_n\), which is, by construction, conflict-free. Suppose for a contradiction that \(S_n \not \subseteq \Gamma_{F}(S_n)\). Then there is an attack \(U \rightsquigarrow_\succ\sigma_n\) on some \(\sigma_n\in S_n\) such that \(U \cap S_n^+ = \emptyset\). Since \(S_n\) is conflict-free, \(U \setminus S_n \neq \emptyset\). Consider some \(\upsilon \in U \setminus S_n\). Since \(\upsilon \not \in S_n\), the set \(S_n \cup \{\upsilon\}\) is not conflict-free, and so there must be some attack that involves but does not target \(\upsilon\). Let \(S_n' \cup \{\upsilon\} \rightsquigarrow_\succ\sigma_n'\) be such an attack, where \(S_n' \subseteq S_n\) and \(\sigma_n' \in S_n\). Since \(S_n\) is conflict-free and \(\upsilon \not \in S_n^+\), this attack is not defended by \(S_n\), i.e. \((S_n' \cup \{\upsilon\}) \cap S_n^+ = \emptyset\). We can thus apply Claim 2, condition (c), to obtain \(\upsilon \not \succ \beta\) for all \(\beta \in S_n' \cup \{\sigma_n'\}\). It follows that we also have the attack \(S_n' \cup \{\sigma_n'\} \rightsquigarrow_\succ\upsilon\), which contradicts \(U \cap S_n^+ = \emptyset\).

We have thus exhibited a set \(S_n \supsetneq S_0\) that is conflict-free and such that \(S_n \subseteq \Gamma_{F}(S_n)\), which contradicts that fact that \(S_0\) is a preferred extension. Having obtained the desired contradiction, we can conclude that every preferred extension of a strongly symmetric PSETAF with a transitive preference relation is also a stable extension. ◻

11 Proofs for Section 6 ↩︎

Lemma 1. Let \(\mathcal{K}_\succ\) be a prioritized KB with \(\mathcal{K}=\langle \mathcal{T}, \mathcal{A}\rangle\) and \(\mathcal{A}'\subseteq\mathcal{A}\). The set \(\mathcal{A}'\) is \(\mathcal{T}\)-consistent iff \(\mathcal{A}'\) is conflict-free in the associated PSETAF \(F_{\mathcal{K}, \succ}\).

Proof. Assume for a contradiction that \(\mathcal{A}'\) is \(\mathcal{T}\)-consistent and not conflict-free. There exists \(\alpha\in \mathcal{A}'\cap\mathcal{A}'^+\), so there exists \(A\subseteq \mathcal{A}'\) such that \(A\rightsquigarrow_\mathcal{K}\alpha\). However, it follows that \((A\cup\{\alpha\})\in\mathit{Conf}(\mathcal{K})\), contradicting the \(\mathcal{T}\)-consistency of \(\mathcal{A}'\).

If \(\mathcal{A}'\) is \(\mathcal{T}\)-inconsistent, there exists \(C\in\mathit{Conf}(\mathcal{K})\) such that \(C\subseteq\mathcal{A}'\). Since \(\succ\) is acyclic and \(C\) is finite, there exists \(\gamma\in C\) such that for every \(\delta\in C\), \(\gamma\not\succ\delta\). It follows that \(C\setminus\{\gamma\}\rightsquigarrow_\mathcal{K}\gamma\). Thus \(\gamma\in C\cap C^+\), i.e., \(C\) is not conflict-free, hence neither is \(\mathcal{A}'\). ◻

Proof. Assume for a contradiction that \(\mathcal{A}'\in\mathit{PRep}(\mathcal{K}_\succ)\) and is not a stable extension of \(F_{\mathcal{K}, \succ}\). By Lemma 1, \(\mathcal{A}'\) is conflict-free so \({\mathcal{A}'}^+\subseteq \mathcal{A}\setminus\mathcal{A}'\). Since \(\mathcal{A}'\) is not stable, there must then exist \(\alpha\in \mathcal{A}\setminus\mathcal{A}'\) such that \(\alpha\notin {\mathcal{A}'}^+\). Since \(\mathcal{A}'\) is a repair, \(\mathcal{A}'\cup\{\alpha\}\) is \(\mathcal{T}\)-inconsistent, and since \(\alpha\notin {\mathcal{A}'}^+\), then for every \(B\subseteq\mathcal{A}'\) such that \(B\cup\{\alpha\}\) is \(\mathcal{T}\)-inconsistent, there exists \(\beta\in B\) such that \(\alpha\succ\beta\). Then \(\mathcal{A}'\setminus\{\beta\mid \alpha\succ\beta\}\cup\{\alpha\}\) is a Pareto improvement of \(\mathcal{A}'\). It follows that \(\mathcal{A}'\notin\mathit{PRep}(\mathcal{K})\).

In the other direction, assume for a contradiction that \(\mathcal{A}'\) is a stable extension of \(F_{\mathcal{K}, \succ}\) and \(\mathcal{A}'\notin\mathit{PRep}(\mathcal{K}_\succ)\). By Lemma 1, since \(\mathcal{A}'\) is stable, \(\mathcal{A}'\) is \(\mathcal{T}\)-consistent. Since \(\mathcal{A}'\notin\mathit{PRep}(\mathcal{K}_\succ)\), it follows that there exists \(\alpha\in\mathcal{A}\setminus\mathcal{A}'\) such that \(\alpha\) is \(\mathcal{T}\)-consistent and for every \(B\subseteq\mathcal{A}'\) such that \(B\cup\{\alpha\}\) is \(\mathcal{T}\)-inconsistent, there exists \(\beta\in B\) such that \(\alpha\succ\beta\). Since \(\mathcal{A}'\) is stable, there exists \(A\subseteq \mathcal{A}'\) such that \(A\rightsquigarrow_\mathcal{K}\alpha\) (otherwise \(\alpha\notin{\mathcal{A}'}^+\)). But then \(A\cup\{\alpha\}\) is \(\mathcal{T}\)-inconsistent, so there exists \(\beta\in A\) such that \(\alpha\succ\beta\), which contradicts \(A\rightsquigarrow_\mathcal{K}\alpha\). ◻

Proof. Let \(\mathcal{K}_\succ\) be a prioritized KB with \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\), and a transitive priority relation \(\succ\). The associated PSETAF is \(F_{\mathcal{K}, \succ}= (\mathcal{A}, \rightsquigarrow_{\mathcal{K}}, \succ)\), where \(\rightsquigarrow_{\mathcal{K}} = \{(C \setminus \{\alpha\}, \alpha) \mid C \in \mathit{Conf}(\mathcal{K}), \alpha \in C\}\).

Let \(F_\mathsf{cl}= (\mathcal{A}, \rightsquigarrow_{\mathcal{K}}, \succ')\) where \(\succ'\) is the transitive closure of \(\succ\). The transitive closure of an acyclic binary relation is acyclic, so \(\succ'\) is an acyclic binary relation over \(\mathcal{A}\), so \(F_\mathsf{cl}\) is a PSETAF. Moreover, observe that \(F_\mathsf{cl}\) is strongly symmetric and \(\succ'\) is transitive, so by Theorem [psetaf-coh], \(F_\mathsf{cl}\) is coherent.

We show that \(F_{\mathcal{K}, \succ}\) and \(F_\mathsf{cl}\) have the same corresponding SETAF, so that \(F_{\mathcal{K}, \succ}\) is coherent. The corresponding SETAF of \(F_{\mathcal{K}, \succ}\) is \((\mathcal{A},\rightsquigarrow_{\mathcal{K},\succ})\), where \(S \rightsquigarrow_{\mathcal{K},\succ} \alpha\) iff \(S \rightsquigarrow_\mathcal{K}\alpha\) and \(\alpha \not \succ \beta\) for every \(\beta \in S\), and the corresponding SETAF of \(F_\mathsf{cl}\) is \((\mathcal{A},\rightsquigarrow_{\mathcal{K},\succ'})\), where \(S \rightsquigarrow_{\mathcal{K},\succ'} \alpha\) iff \(S \rightsquigarrow_\mathcal{K}\alpha\) and \(\alpha \not \succ' \beta\) for every \(\beta \in S\). Since \(\succ\subseteq\succ'\), we thus have \(\rightsquigarrow_{\mathcal{K},\succ'}\subseteq\rightsquigarrow_{\mathcal{K},\succ}\). Assume for a contradiction that there exists \(S\rightsquigarrow_{\mathcal{K},\succ}\alpha\) such that \(S\not\rightsquigarrow_{\mathcal{K},\succ'}\alpha\). There must be \(\beta\in S\) such that \(\alpha\succ'\beta\). Since \(\succ'\) is the transitive closure of \(\succ\), it follows that there exists \(\gamma_1,\dots,\gamma_n\) such that \(\alpha\succ\gamma_1\succ\dots\succ\gamma_n\succ\beta\). But then, since \(\{\alpha,\beta\}\subseteq S\cup\{\alpha\}\in\mathit{Conf}(\mathcal{K})\) and \(\succ\) is a transitive priority relation, it follows that \(\alpha\succ\beta\). Hence \(S\not\rightsquigarrow_{\mathcal{K},\succ}\alpha\). We conclude that \(\rightsquigarrow_{\mathcal{K},\succ'}=\rightsquigarrow_{\mathcal{K},\succ}\) and that\(F_{\mathcal{K}, \succ}\) and \(F_\mathsf{cl}\) have the same corresponding SETAF. ◻

Proof. Since \(\mathcal{B}\in\mathit{PRep}(\mathcal{K}_\succ)\), by Theorem [tstable], \(\mathcal{B}\) is a stable extension of \(F_{\mathcal{K}, \succ}\). Since every stable extension is also a complete extension, and \(\mathcal{G}\) is the \(\subseteq\)-minimal complete extension of \(F_{\mathcal{K}, \succ}\), it follows that \(\mathcal{G}\subseteq\mathcal{B}\). ◻

Proof. Let \(\mathcal{G}\) be the grounded extension of \(F_\mathcal{K}\) and \(\mathcal{A}^\cap\) be the intersection of the repairs of \(\mathcal{K}\). Let \(\alpha\in\mathcal{A}^\cap\). There is no \(C\in\mathit{Conf}(\mathcal{K})\) such that \(\alpha\in C\) (otherwise \(C\setminus\{\alpha\}\) would be \(\mathcal{T}\)-consistent and could be extended to a repair of \(\mathcal{K}\) that would not contain \(\alpha\)). Thus there is no \(A\rightsquigarrow_\mathcal{K}\alpha\). It follows that \(\alpha\in \Gamma_{F_\mathcal{K}}(\emptyset)\subseteq\mathcal{G}\). Hence \(\mathcal{A}^\cap\subseteq\mathcal{G}\). In the other direction, let \(\mathcal{A}'\in\mathit{SRep}(\mathcal{K})\). Since \(\succ_\emptyset\) is the empty relation, then \(\mathit{SRep}(\mathcal{K})=\mathit{PRep}(\mathcal{K}_{\succ_\emptyset})\), so \(\mathcal{A}'\in\mathit{PRep}(\mathcal{K}_{\succ_\emptyset})\) and by Theorem [ground-pareto], \(\mathcal{G}\subseteq\mathcal{A}'\). It follows that \(\mathcal{G}\subseteq\mathcal{A}^\cap\). ◻

Proof. Let \(\alpha\in \mathit{Elect}(\mathcal{K}_\succ)\) and \(F=(\mathcal{A}, \rightsquigarrow_{\mathcal{K},\succ})\) be the SETAF corresponding to \(F_{\mathcal{K},\succ}\). Since for every \(C\in\mathit{Conf}(\mathcal{K})\) such that \(\alpha\in C\), there exists \(\beta\in C\) such that \(\alpha\succ\beta\), there is no \(C\in\mathit{Conf}(\mathcal{K})\) such that \(C\setminus\{\alpha\}\rightsquigarrow_{\mathcal{K},\succ}\alpha\), so no \(S\subseteq \mathcal{A}\) such that \(S\rightsquigarrow_{\mathcal{K},\succ}\alpha\). It follows that \(\alpha\in \Gamma_{F}(\emptyset)\subseteq \mathcal{G}\). ◻

Proof. We adapt the proof of P-hardness for the problem of deciding whether an argument belongs to the grounded extension of an argumentation framework given in [49] (Reduction 3.8). We modify the original log-space reduction from deciding whether a variable is in the minimal model of a definite Horn formula so that the argument framework does not contain cycles, which are not allowed in our setting. Let \(\varphi=\{r_l: b_{l,1}\wedge\dots\wedge b_{l,i_l}\rightarrow h_l\mid 1\leq l\leq n\}\) be a definite Horn formula over the set of variables \(X\), and let \(z\in X\) be the variable we want to decide whether it belongs to the minimal model of \(\varphi\). We assume w.l.o.g. that for every \(r_l\), \(h_l\neq b_{l,j}\) for all \(j\).

We construct a DL-Lite\(_{\mathsf{core}}\) KB \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\) and priority relation as follows. \[\begin{align} \mathcal{T}=&\{ \exists \mathit{FalseInBod}^-\sqsubseteq \neg \exists \mathit{SatBodHead}, \exists \mathit{SatBodHead}^-\sqsubseteq \neg\exists \mathit{FalseInBod}, \exists \mathit{FalseInBod}\sqsubseteq \neg T\}\\ \mathcal{A}=&\{\mathit{FalseInBod}(b_{l,j},r_l)\mid r_l\in\varphi, 1\leq j\leq i_l \}\cup\{\mathit{SatBodHead}(r_l, h_l)\mid r_l\in\varphi\}\cup\{T(z)\} \end{align}\] \[\mathit{SatBodHead}(r_l, x)\succ \mathit{FalseInBod}(x,r_{l'})\] Clearly, \(\succ\) is acyclic. We show that \(T(z)\) belongs to the grounded extension \(\mathcal{G}\) of \(F_{\mathcal{K},\succ}\) iff \(z\) belongs to the minimal model of \(\varphi\). The corresponding AF \(F=(\mathcal{A}, \rightsquigarrow_{\mathcal{K},\succ})\) of \(F_{\mathcal{K},\succ}\) is such that \[\begin{align} \rightsquigarrow_{\mathcal{K},\succ}=&\{(\mathit{SatBodHead}(\_, x), \mathit{FalseInBod}(x,\_))\mid x\in X\}\cup\\& \{(\mathit{SatBodHead}(r_l, \_), \mathit{FalseInBod}(\_,r_l)), (\mathit{FalseInBod}(\_,r_l), \mathit{SatBodHead}(r_l, \_))\mid r_l\in\varphi\}\cup\\ &\{(T(z), \mathit{FalseInBod}(z,\_)), ( \mathit{FalseInBod}(z,\_),T(z))\} \end{align}\] The intuition behind the reduction is that an argument \(\mathit{SatBodHead}(r_l, x)\) is in \(\mathcal{G}\) iff all variables in the body of \(r_l\) are in the minimal model of \(\varphi\), so that \(x\) is also in this model, and that an argument \(\mathit{FalseInBod}(x,\_)\), stating that \(x\) is not in the model, is attacked by \(\mathcal{G}\) only if \(x\) is in the model. That is, when computing \(\mathcal{G}\) via iteratively applying the characteristic function \(\Gamma_{F}\) we simulate the following algorithm for deciding whether \(z\) is in the minimal model of \(\varphi\). The algorithm starts with the rules with empty body and adds their rule heads to the minimal model: \(\Gamma_{F}(\emptyset)=\{\mathit{SatBodHead}(r_l, x)\mid\text{there is no }\mathit{FalseInBod}(\_,r_l)\in\mathcal{A}\}\cup\{T(z)\text{ if there is no }\mathit{FalseInBod}(z,\_)\in\mathcal{A}\}\). Then it iteratively considers all rules with the body already being part of the minimal model and adds their heads to the minimal model until a fixed-point is reached: if \(G_i\) is the result at step \(i\), let \(S_i=\{\mathit{FalseInBod}(y,\_)\mid \mathit{SatBodHead}(\_, y)\in G_i\}\) be the set of arguments that are attacked by \(G_i\), \(\Gamma_{F}(G_i)=\{\mathit{SatBodHead}(r_l, x)\mid\text{there is no }\mathit{FalseInBod}(\_,r_l)\in \mathcal{A}\setminus S_i\}\cup\{T(z)\text{ if there is no }\mathit{FalseInBod}(z,\_)\in \mathcal{A}\setminus S_i\}\). We then have that \(z\) is in the minimal model of the Horn-formula \(\varphi\) iff \(T(z)\in \mathcal{G}\). This shows the \(\mathrm{\small P}\)-hardness of assertion entailment as well as of verifying \(\mathcal{G}\). ◻

We recall the definition of well-founded semantics and introduce some notation and terminology. Our presentation is loosely based upon Chapter 15 from [50], but tailored (and simplified) to suit our purposes. We refer readers to the latter chapter for a more detailed introduction to the semantics of rule languages with negation.

A normal logic program (aka Datalog\(^\neg\) program, henceforth abbreviated to program) is a finite set of rules of the form \(\rho= \mathtt{h} \leftarrow \mathtt{b}_1, \ldots, \mathtt{b}_n, \neg\;\mathtt{b}_{n+1}, \ldots, \neg\;\mathtt{b}_{n+m}\), where each \(\mathtt{b}_i\) is an atom \(\mathtt{p}(t_1, \ldots,t_n)\) whose every term \(t_i\) is either a constant or a variable. The atom \(\mathtt{h}\) is called the head of the rule \(\rho\), and the body of \(\rho\) is \(\mathtt{b}_1, \ldots, \mathtt{b}_n, \neg\;\mathtt{b}_{n+1}, \ldots, \neg\;\mathtt{b}_{n+m}\). The atoms \(\mathtt{b}_1, \ldots, \mathtt{b}_n\) are called positive body atoms, while the atoms \(\mathtt{b}_{n+1}, \ldots, \mathtt{b}_{n+m}\) (which are preceded by \(\neg\)) are called negative body atoms. As is common, we require rules to satisfy the following safety condition: every variable that appears in the head atom of a rule must occur in some positive body atom of that rule. Note that it is allowed for the body of a rule to be empty (empty ruleheads can also be considered, but will not be used in what follows).

A definite rule is a rule that does not contain any negative body atoms, and a definite program is a finite set of definite rules. A ground atom (resp.rule, program) is an atom (resp.rule, program) that does not contain any variables. We will sometimes use the term fact in place of ground atom. Given any program \(\Pi\), the grounding of \(\Pi\), denoted \(grnd(\Pi)\), consists of all ground rules that can be obtained from a rule in \(\Pi\) by instantiating its variables with constants occurring in \(\Pi\).

Given a ground program \(\Pi\), we let \(B_\Pi\) consist of all facts that appear (positively or negatively) in \(\Pi\). A 2-valued instance \(\mathbf{I}\) for \(\Pi\) assigns to each fact in \(B_\Pi\) a value that is either true or false. We denote by \(\bot\) the 2-valued instance that assigns false to all facts in \(B_\Pi\). A 3-valued instance for \(\Pi\) is defined similarly, except now there are three possible values: true, unknown, or false. It will be convenient to view 2-valued instances as sets of (positive) facts, where a fact is assigned true if it belongs to the set, and otherwise, is assigned false. Similarly, a 3-valued instance can be given as a consistent set of literals (possibly negated facts), where facts appearing positively in the set are assigned true, those whose negation is in the set are assigned false, and all other facts are treated as unknown. We use the notation \(\mathbf{I}(\mathtt{a})\) to refer to the truth value that \(\mathbf{I}\) assigns to the fact \(\mathtt{a}\).

Given two 3-valued instances \(\mathbf{I}\) and \(\mathbf{J}\), we write \(\mathbf{I} < \mathbf{J}\) to mean that \(\mathbf{I}(\mathtt{a}) < \mathbf{J}(\mathtt{a})\) for ever ground atom \(\mathtt{a}\), where the truth values are ordered as follows: false \(<\) unknown \(<\) true. A (2-valued) model of a ground definite program \(\Pi\) is a 2-valued instance for \(\Pi\) such that for every rule \(\rho \in \Pi\), if all body atoms in \(\rho\) are assigned true, then the head atom is also assigned true. It is known that every ground definite program has a unique minimal model, i.e., a model \(\mathbf{I}\) such that \(\mathbf{I} < \mathbf{J}\) for every model \(\mathbf{J}\). We denote by \(mm(\Pi)\) the minimal model of a ground definite program \(\Pi\).

We next extend minimal models to stratified programs. A stratification of a program \(\Pi\) is a sequence \(\Pi^{1}, \ldots, \Pi^n\) and a function \(\sigma\) mapping predicates to \([1,n]\) such that the following conditions hold:

\(\Pi\) is the disjoint union of \(\Pi^{1}, \ldots, \Pi^n\)
for every predicate \(P\) that occurs in \(\Pi\), all rules that have \(P\) in the head belong to \(\Pi^{\sigma(P)}\)
for every \(1 \leq i \leq n\):
- if predicate \(P\) occurs positively in the body of some rule of \(\Pi^i\), then \(\sigma(P) \leq i\)
- if predicate \(P\) occurs negatively in the body of a rule of \(\Pi^i\), then \(\sigma(P) < i\)

A program \(\Pi\) is stratified if there exists a stratification for \(\Pi\). Given a program \(\Pi\) with stratification \(\Pi^{1}, \ldots, \Pi^n\), we proceed as follows. We start by computing the grounding \(grnd(\Pi)\), and let \(gr(\Pi^{1}), \ldots, gr(\Pi^n)\) be the ground programs corresponding to \(\Pi^{1}, \ldots, \Pi^n\) (note that they are grounded w.r.t.all constants occurring in \(\Pi\), not just the constants from the stratum). We set \(M_1\) equal to the minimal model of the ground definite program \(gr(\Pi^{1})\). Then for \(1 \leq i < n\), we let \(M_{i+1} = M_i \cup M'_{i+1}\), where \(M'_{i+1}\) is the minimal model of the ground definite program obtained from \(gr(\Pi^{i+1}\)) by (i) deleting every rule whose body contains \(\neg\mathtt{a}\) where \(\mathtt{a}\in M_i\), and (ii) removing all negative facts from the remaining rule bodies. We call \(M_n\) the minimal model of \(\Pi\).

We now proceed to the definition of the well-founded semantics, which can be applied to arbitary programs. For every ground program \(\Pi\) and 2-valued instance¹ \(\mathbf{I}\) for \(\Pi\), we denote by \(\Pi|_\mathbf{I}\) the ground definite program that is obtained from \(\Pi\) as follows: (i) delete every rule whose body contains \(\neg\mathtt{a}\) where \(\mathtt{a}\in \mathbf{I}\), (ii) remove all negative body atoms from the remaining rules. We then consider the following infinite sequence of 2-valued instances: \[\mathbf{I}_0 = \bot \qquad \mathbf{I}_{i+1} = mm(\Pi|_{\mathbf{I}_i})\] It is known (and can be readily verified) that for every \(i > 0\), we have: \[\mathbf{I}_0 < \mathbf{I}_2 < \ldots <\mathbf{I}_{2i} < \mathbf{I}_{2i+2} < \mathbf{I}_{2i+1} < \mathbf{I}_{2i-1} < \ldots < \mathbf{I}_{1}\] As there are a finite number of possible instances, the sequences \((\mathbf{I}_{2i})_{i \geq 0}\) and \((\mathbf{I}_{2i+1})_{i \geq 0}\) both reach a fixpoint. We let \(\mathbf{I}_*\) denote the limit of the increasing sequence \((\mathbf{I}_{2i})_{i \geq 0}\), and let \(\mathbf{I}^*\) denote the limit of the decreasing sequence \((\mathbf{I}_{2i+1})_{i \geq 0}\). Then the (unique) well-founded model of \(\Pi\) is the 3-valued instance that assigns true to all facts \(\mathtt{a}\) such that \(\mathtt{a}\in \mathbf{I}_*\), assigns false to all facts \(\mathtt{a}\) such that \(\mathtt{a}\not \in \mathbf{I}^*\), and unknown to all other facts. If \(\Pi\) is an arbitrary (not necessarily ground) program, then the well-founded model of \(\Pi\) is defined as the well-founded model of \(grnd(\Pi)\).

It is known that if \(\Pi\) is stratified, then the well-founded model of \(\Pi\) is equal to the minimal model of \(\Pi\). More precisely, if \(\Pi\) has a stratification with \(p\) levels, then \(\mathbf{I}_{2p}\) is the minimal model, and we have \(\mathbf{I}_{2p} = \mathbf{I}_{2p+i}\) for all \(i \geq 0\).

We recall the following result from [33] (very slightly modified to suit our later extensions) that shows how to compute the grounded extension of an AF via well-founded semantics. It makes reference to the following two rules: \[r_{\mathtt{acc}}: \mathtt{acc}(x) \leftarrow \mathtt{arg}(x), \neg\mathtt{def}(x) \qquad r_{\mathtt{def}}: \mathtt{def}(x) \leftarrow \mathtt{attack}(y,x), \mathtt{acc}(y)\]

Theorem 9. Let \(F=(\mathit{Args},\rightsquigarrow)\) be an AF. Then \(E \subseteq \mathit{Args}\) is the grounded extension of \(F\) iff \[\{\mathtt{acc}(\alpha), \neg \mathtt{def}(\alpha) \mid \alpha \in E\} \cup \{\mathtt{def}(\beta), \neg \mathtt{acc}(\beta) \mid \beta \in E^+\} \cup \{\mathtt{attack}(\alpha, \beta) \mid \alpha \rightsquigarrow\beta\} \cup \{\mathtt{arg}(\alpha) \mid \alpha \in \mathit{Args}\}\] is the well-founded model of the program \(\{r_{\mathtt{acc}}, r_{\mathtt{def}}\} \cup \{\mathtt{attack}(\alpha, \beta) \leftarrow \, \mid \alpha \rightsquigarrow\beta\}\cup \{\mathtt{arg}(\alpha) \leftarrow \, \mid \alpha \in \mathit{Args}\}\).

The following theorem generalizes the preceding result to \(k\)-SETAFs, i.e., SETAFs for which \(S \rightsquigarrow\beta\) implies \(|S| \leq k\). We will use relations \(\mathtt{attack}_1, \ldots, \mathtt{attack}_k\) to store attacks, where \(\mathtt{attack}_i(\alpha_1, \ldots, \alpha_i, \beta)\) specifies that there is an attack \(\{\alpha_1, \ldots, \alpha_i\} \rightsquigarrow\beta\). We will use the following variants of rule \(r_{\mathtt{def}}\), where \(i\) ranges from \(1\) to \(k\): \[r_{\mathtt{def}}^{i}: \mathtt{def}(x) \leftarrow \mathtt{attack}_i(y_1, \ldots, y_i,x), \mathtt{acc}(y_1), \ldots, \mathtt{acc}(y_i)\]

Theorem 8. Let \(F=(\mathit{Args},\rightsquigarrow)\) be a \(k\)-SETAF. Then \(\alpha\) is in the grounded extension of \(F\) iff \(\mathtt{acc}(\alpha)\) belongs to the well-founded model of the following normal logic program: \[\begin{align} &\{\mathtt{def}(x) \leftarrow \mathtt{att}_i(y_1,.., y_i,x), \mathtt{acc}(y_1),...,\mathtt{acc}(y_i) \mid 1 \leq i \leq k\} \cup \{\mathtt{acc}(x) \leftarrow \mathtt{arg}(x), \neg\mathtt{def}(x)\} \\ &\cup \{\mathtt{arg}(\alpha) \mid \alpha \in \mathit{Args}\} \cup \{\mathtt{att}_i(\alpha_1, \ldots, \alpha_i, \beta) \leftarrow \, \mid \{\alpha_1, \ldots, \alpha_i\} \rightsquigarrow\beta\} \end{align}\]

Proof. Let \(\Pi_F= \{r_{\mathtt{acc}}, r_{\mathtt{def}}^1, \ldots, r_{\mathtt{def}}^k\} \cup \{\mathtt{arg}(\alpha) \mid \alpha \in \mathit{Args}\} \cup \{\mathtt{attack}_i(\alpha_1, \ldots, \alpha_i, \beta) \leftarrow \, \mid \{\alpha_1, \ldots, \alpha_i\} \rightsquigarrow\beta\}\), and let us consider the sequence of sets produced during the computation of the well-founded model of \(\Pi_F\). A straightforward inductive argument shows that the following statements holds for every \(j \geq 0\): \[\begin{align} \mathbf{I}_{2j +2} &= S_{\mathtt{arg}} \cup S_{\mathtt{attack}} \cup \{\mathtt{acc}(\alpha) \mid \alpha \in \Gamma_{F}^{j+1}(\emptyset)\} \cup \{\mathtt{def}(\beta) \mid \beta \in (\Gamma_{F}^{j+1}(\emptyset))^+ \}\\ \mathbf{I}_{2j +1} &= S_{\mathtt{arg}} \cup S_{\mathtt{attack}} \cup \{\mathtt{acc}(\alpha) \mid \alpha \in \mathit{Args}\setminus (\Gamma_{F}^{j}(\emptyset))^+ \} \cup \{\mathtt{def}(\beta) \mid \beta \in (\mathit{Args}\setminus (\Gamma_{F}^{j}(\emptyset))^+)^+ \} \end{align}\] where \(S_{\mathtt{arg}}= \{\mathtt{arg}(\alpha) \mid \alpha \in \mathit{Args}\}\), \(S_{\mathtt{attack}}=\{\mathtt{attack}_i(\alpha_1, \ldots, \alpha_i, \beta)\mid \{\alpha_1, \ldots, \alpha_i\} \rightsquigarrow\beta\}\) and \((\Gamma_{F}^{0}(\emptyset))^+=\emptyset\). Recall that these are 2-valued instances, so we list the positive facts, with all other facts being assigned false.

Now let \(E\) be the grounded extension of \(F\). Then there is \(\ell\) such that \(E = \Gamma_{F}^{\ell}(\emptyset)\), and \(\Gamma_{F}^{\ell+j}(\emptyset)=\Gamma_{F}^{\ell}(\emptyset)\) for all \(j \geq 1\). Then we have: \[\begin{align} \mathbf{I}_* &= S_{\mathtt{arg}} \cup S_{\mathtt{attack}} \cup \{\mathtt{acc}(\alpha) \mid \alpha \in \Gamma_{F}^{\ell}(\emptyset)\} \cup \{\mathtt{def}(\beta) \mid \beta \in (\Gamma_{F}^{\ell}(\emptyset))^+ \}\\ &= S_{\mathtt{arg}} \cup S_{\mathtt{attack}} \cup \{\mathtt{acc}(\alpha) \mid \alpha \in E\} \cup \{\mathtt{def}(\beta) \mid \beta \in E^+ \}\\ \mathbf{I}^* &= S_{\mathtt{arg}} \cup S_{\mathtt{attack}} \cup \{\mathtt{acc}(\alpha) \mid \alpha \in \mathit{Args}\setminus (\Gamma_{F}^{\ell}(\emptyset))^+ \} \cup \{\mathtt{def}(\beta) \mid \beta \in (\mathit{Args}\setminus (\Gamma_{F}^{\ell}(\emptyset))^+)^+ \}\\ &= S_{\mathtt{arg}} \cup S_{\mathtt{attack}} \cup \{\mathtt{acc}(\alpha) \mid \alpha \in \mathit{Args}\setminus E^+ \} \cup \{\mathtt{def}(\beta) \mid \beta \in (\mathit{Args}\setminus E^+)^+ \} \end{align}\] Note that if \(\beta \not \in (\mathit{Args}\setminus E^+)^+\), then for every \(S \rightsquigarrow\beta\), there exists \(\gamma \in S\) such that \(\gamma \in E^+\). It follows that \(\beta \in \Gamma_{F}(E)=E\). We therefore have that the well-founded model of \(\Pi_F\) is equal to \[S_{\mathtt{arg}} \cup S_{\mathtt{attack}} \cup \{\mathtt{acc}(\alpha), \neg \mathtt{def}(\alpha) \mid \alpha \in E\} \cup \{\mathtt{def}(\beta), \neg \mathtt{acc}(\beta) \mid \beta \in E^+ \}\] which completes the proof. ◻

Next we need to define rules to compute conflicts, in order to derive which attack facts should be included. We assume that we have a finite set \(Q_{\mathsf{unsat}}\) of BCQs such that \(\mathcal{A}\) is \(\mathcal{T}\)-consistent iff no \(q \in Q_{\mathsf{unsat}}\) evaluates to true on \(\mathcal{A}\) (or more formally, on the interpretation \(\mathcal{I}_\mathcal{A}\) based upon \(\mathcal{A}\)). Note that when \(\mathcal{T}\) is formulated in DL-Lite\(^{\mathcal{H}}_\mathsf{horn}\), such a set \(Q_{\mathsf{unsat}}\) can be computed using standard query rewriting procedures. In what follows, we let \(N\) be the maximal number of conjuncts in any BCQ in \(Q_{\mathsf{unsat}}\).

To be able to identify conflicts, and later repairs, we assume that each assertion has an additional final argument that contains a unique id for that assertion, e.g. \(A(a,u_5), R(a,b,u_{17})\). Given a (standard) ABox \(\mathcal{A}\), we will use \(\mathcal{A}_{id}\) to denote a corresponding set of annotated assertions, and for every \(\alpha \in \mathcal{A}\), we let \(id(\alpha)\) be the id of the corresponding atom in \(\mathcal{A}_{id}\). We will store the priority relation in a binary relation \(\mathtt{pref}\) over assertion ids, with \(\mathtt{pref}(id(\alpha), id(\beta))\) meaning that \(\alpha \succ \beta\). We let \(Q_{\mathsf{unsat}}^*\) consist of all BCQs \(q^*\) that can be obtained from some \(q \in Q_{\mathsf{unsat}}\) as follows: (i) order the atoms in \(q\), and (ii) add a final argument \(z_j\) to the \(j\)th atom (where \(z_j\) is a fresh variable not occurring in \(Q_{\mathsf{unsat}}\) and distinct from \(z_k\) with \(k \neq j\)).

We introduce predicates \(\mathtt{confl}_i\) for \(i=1, \ldots, N\), which will store conflicts that involve exactly \(i\) assertions. Concretely, for each BCQ \(q^* \in Q_{\mathsf{unsat}}^*\) with a single atom we have the following rule (which can be omitted if we assume no self-contradicting assertions): \[\mathtt{confl}_0(z_1) \leftarrow q^*(z_1)\] and for every BCQ \(q^* \in Q_{\mathsf{unsat}}^*\) with \(k+1\) atoms, we have: \[\mathtt{confl}_{k}(z_1, \ldots, z_k, z_{k+1}) \leftarrow q^*(z_1, \ldots, z_k, z_{k+1}), \bigwedge_{\substack{0 \leq j < k\\ (z_{\ell_1}, \ldots, z_{\ell_j}, z_{\ell_{j+1}}) \in \{z_1, \ldots, z_k, z_{k+1}\}^{j+1}}} \neg\mathtt{confl}_{j}(z_{\ell_1}, \ldots, z_{\ell_j}, z_{\ell_{j+1}})\] Here we write \(q^*(z_1, \ldots, z_k)\) to highlight the shared variables \(z_j\), but \(q^*\) will contain also the original variables in the BCQ \(q\). Observe that negated body atoms are used to ensure subset minimality. We can then compute the attack relations by using the following rule for every \(1 \leq i < N\): \[r_{\mathtt{att}}^{i}: \mathtt{attack}_i(z_1, \ldots, z_i, z_{i+1}) \leftarrow \mathtt{confl}_{i}(z_1, \ldots, z_i, z_{i+1}), \neg\mathtt{pref}(z_{i+1}, z_1), \ldots, \neg\mathtt{pref}(z_{i+1}, z_i)\] where We generate the set of arguments (corresponding to ids of assertions that are not self-contradictory) by means of the following rules, for every concept name \(A\) and role name \(R\): \[\mathtt{arg}(z_1) \leftarrow A(x,z_1), \neg\mathtt{confl}_0(z_1) \qquad \mathtt{arg}(z_1) \leftarrow R(x,y,z_1), \neg\mathtt{confl}_0(z_1)\] Let \(\Pi_{\mathtt{confl}}\) be the preceding set of rules. We observe that \(\Pi_{\mathtt{confl}}\) is stratified. It is not hard to see that these rules allow us to compute the conflicts, and hence the attacks in the SETAF corresponding to the PSETAF \(F_{\mathcal{K}, \succ}\). Specifically, we have:

Lemma 2. Let \(F=(\mathit{Args}, \rightsquigarrow_\succ)\) be the corresponding SETAF for the PSETAF \(F_{\mathcal{K}, \succ}\) based upon the prioritized KB \(\mathcal{K}_\succ\). The following statements are equivalent:

\(\{\alpha_1, \ldots, \alpha_n\} \rightsquigarrow_\succ \beta\)
the atom \(\mathtt{attack}_n(id(\alpha_1), \ldots, id(\alpha_{n}), id(\beta))\) belongs to the minimal model of \(\Pi_{\mathtt{confl}} \cup \{\gamma \leftarrow \, \mid \gamma \in \mathcal{A}_{id}\} \cup \{ \mathtt{pref}(id(\alpha), id(\beta))\mid \alpha \succ \beta\}\).

Intuitively, we want to construct a program that first computes the minimal model of the stratified program \(\Pi_{\mathtt{confl}}\), then uses the attack and conflict facts from this model as input for the ‘argumentation’ program \[\Pi_{\mathtt{arg}}=\{r_{\mathtt{acc}}, r_{\mathtt{def}}^1, \ldots, r_{\mathtt{def}}^N\}\] However, if we simply apply well-founded semantics to the combined program, we might not get the desired result: while we are ‘waiting’ for the computation of the stratified rules to finish, there could be some incorrectly derived \(\mathtt{confl}_{i}\) facts, which could lead to wrongly derived \(\mathtt{attack}\) and \(\mathtt{def}\) facts, in turn wrongly eliminating some \(\mathtt{acc}\) facts.

The following lemma provides a means of safely combining the two programs to achieve the desired result. The basic idea is to delay the application of rules in the second program until the initial stratified program has stabilized. We note that the lemma is tailored to our purposes, and some of the hypotheses could be relaxed at the cost of a more involved proof.

Lemma 3. Let \(\Pi_1\) and \(\Pi_2\) be programs verifying the following conditions: (i) \(\Pi_1\) is stratified and does not use any predicate / fact that occurs in the head of a rule from \(\Pi_2\), and (ii) \(\Pi_2\) may only use predicates / facts from \(\Pi_1\) in the body of rules and in positive form. Then we can construct a program \(\Pi_{1 \rightarrow 2}\) such that the following models contain precisely the same (positive) facts over the relations in \(\Pi_2\):

the well-founded model of \(\Pi_{1\rightarrow 2}\)
the well-founded model of \(\Pi_2 \cup \{\alpha \leftarrow \, \mid \alpha \in mm(\Pi_1)\}\)

Proof. Suppose that \(\Pi_1\) has a stratification with \(p\) levels. Consider the following auxiliary program: \[\Pi_p = \{\mathtt{odd}(x) \leftarrow \mathtt{next}(y,x), \neg\mathtt{odd}(y)\} \cup \{\mathtt{next}(i, i+1) \leftarrow \, \mid 0 \leq i <2p\}\] We assume that the predicate names \(\mathtt{odd}, \mathtt{next}\) and constants \(0, 1, \ldots, 2p\) do not occur in either \(\Pi_1\) or \(\Pi_2\) (otherwise, we can choose other fresh names / constants). A straightforward induction shows that the following instances will be produced during the construction of the well-founded model of \(\Pi_p\): \[\begin{align} \mathbf{I}_{2j +2} &= \{\mathtt{odd}(i) \mid 1\leq i\leq 2p, i < 2j+2, \text{ and } i \text{ is odd } \} \cup \{\mathtt{next}(i, i+1) \mid 0 \leq i <2p\}\\ \mathbf{I}_{2j +1} &= \{\mathtt{odd}(i) \mid 1\leq i\leq 2p \text{ and either } i \text{ is odd or } i > 2j+1 \} \cup \{\mathtt{next}(i, i+1) \mid 0 \leq i <p\} \end{align}\] In particular, this means that the instance \(\mathbf{I}_{2p}\), and every later instance in the sequence, contains \[\neg\mathtt{odd}(0), \mathtt{odd}(1), \neg\mathtt{odd}(2), \ldots, \mathtt{odd}(2p-1), \neg\mathtt{odd}(2p)\] but none of the earlier instances contains precisely this combination of positive and negative facts.

Let us now modify the rules in \(\Pi_2\) as follows: add \(\neg\mathtt{odd}(0), \mathtt{odd}(1), \neg\mathtt{odd}(2), \ldots, \mathtt{odd}(2p-1), \neg\mathtt{odd}(2p)\) to the body of each rule \(r\) (denoting the result \(r'\)). Let \(\Pi_2'\) be the resulting set of rules.

Now consider the program \(\Pi_{1\rightarrow 2}=\Pi_1 \cup \Pi_2' \cup \Pi_p\) and let \(\mathbf{J_0}, \mathbf{J}_1, \mathbf{J}_2, \ldots\) be the sequence of instances obtained during the construction of the well-founded model of \(grnd(\Pi_1 \cup \Pi_2' \cup \Pi_p)\). We consider the three parts of the program:

Sub-program \(\Pi_1\): Due to the assumptions on \(\Pi_1\), and the safety condition on rules that ensures all head variables occur in a positive body atom, it is not hard to show that for every \(i \geq 2p\), \(\mathbf{J}_i\) contains the same positive facts as the minimal model of \(\Pi_1\), when restricted to predicates and facts from \(\Pi_1\). Specifically, we have:
- every \(\alpha \in mm(\Pi_1)\) belongs to \(\mathbf{J}_i\)
- if \(\alpha \in \mathbf{J}_i\) and \(\alpha\) uses a predicate from \(\Pi_1\), then \(\alpha \in mm(\Pi_1)\)
Sub-program \(\Pi_p\): The rule \(\mathtt{odd}(x) \leftarrow \mathtt{next}(y,x), \neg\mathtt{odd}(y)\) is guarded by the predicate \(\mathtt{next}\) which only occurs in \(\Pi_p\) and which can only match the concrete facts given in \(\Pi_p\). It follows that \(\mathbf{J}_i\) and \(\mathbf{I}_i\) contain precisely the same positive \(\mathtt{odd}\) and \(\mathtt{next}\) facts for every \(i \geq 0\). In particular, the set of literals \(\{\neg\mathtt{odd}(0), \mathtt{odd}(1), \neg\mathtt{odd}(2), \ldots, \mathtt{odd}(2p-1), \neg\mathtt{odd}(2p)\}\) belongs to \(\mathbf{J}_i\) for every \(i \geq 2p\), and it is not contained in \(\mathbf{J}_i\) for \(i < 2p\).
Sub-program \(\Pi_2'\): Every rule in \(\Pi_2'\) contains \(\neg\mathtt{odd}(0), \mathtt{odd}(1), \neg\mathtt{odd}(2), \ldots, \mathtt{odd}(2p-1), \neg\mathtt{odd}(2p)\) in its body. It follows from the preceding point that this set of literals is not contained in \(\mathbf{J}_i\) for \(i < 2p\). Thus, for \(i < 2p\), the rules of \(\Pi_2'\) cannot fire. For every \(i \geq 2p\), the set of literals \(\{\neg\mathtt{odd}(0), \mathtt{odd}(1), \neg\mathtt{odd}(2), \ldots, \mathtt{odd}(2p-1), \neg\mathtt{odd}(2p)\}\) belongs to \(\mathbf{J}_i\), so the rules in \(\Pi_2'\) behave henceforth like the original rules in \(\Pi_2\). Moreover, as noted above, when \(i \geq 2p\), the instance \(\mathbf{J}_i\) contains the same facts as \(mm(\Pi_1)\) w.r.t.predicates / facts from \(\Pi_1\), so the same rule applications that were possible using \(\{\alpha \leftarrow \, \mid \alpha \in mm(\Pi_1)\}\) can be reproduced in \(\Pi_{1\rightarrow 2}\) starting from timepoint \(2p\). Conversely, due to the safety condition on \(\Pi_2\), all applications of rules from \(\Pi_2'\) used to generate the instances \(\mathbf{J}_{2p}, \mathbf{J}_{2p+1}, \ldots\) can be reproduced by the program \(\Pi_2 \cup \{\alpha \leftarrow \, \mid \alpha \in mm(\Pi_1)\}\). It follows that the well-founded model of \(\Pi_{1\rightarrow 2}\) and the well-founded model of \(\Pi_2 \cup \{\alpha \leftarrow \, \mid \alpha \in mm(\Pi_1)\}\) contain precisely the same positive facts when restricted to the relations / facts in \(\Pi_2\).

◻

It is easily verified that \(\Pi_{\mathtt{confl}}\) and \(\Pi_{\mathtt{arg}}\) satisfy the conditions of programs \(\Pi_1\) and \(\Pi_2\) of the preceding lemma. We can therefore combine Theorem 8 and Lemmas 2 and 3 to obtain the following result. While stated for DL-Lite\(^{\mathcal{H}}_\mathsf{horn}\), the result holds for any constraint / ontology language for which conflicts can be identified by a finite set of CQs that depends solely on the ontology / constraints.

A natural under-approximation of the grounded extension is obtained by considering \(\Gamma_{F}^d(\emptyset)\) for some fixed number \(d\). We describe how to adapt the preceding program to compute such an approximation. Essentially, we need to replace the rules \(r_{\mathtt{acc}}, r_{\mathtt{def}}^{i}\) by the following stratified set of rules (recall that \(N\) is the maximal cardinality of conflicts): \[\begin{align} \mathtt{acc}_1(x) &\leftarrow \mathtt{arg}(x)&&\\ \mathtt{def}_1(x) &\leftarrow \mathtt{attack}_i(y_1, \ldots, y_i, x), \mathtt{acc}_{1}(y_1), \ldots, \mathtt{acc}_{1}(y_i) &&1 \leq i < N\\ \mathtt{acc}_{j+1}(x) &\leftarrow \mathtt{arg}(x), \neg\mathtt{def}_{j}(x) && 1 \leq j < 2d \\ \mathtt{def}_{j+1}(x) &\leftarrow \mathtt{attack}_i(y_1, \ldots, y_i, x), \mathtt{acc}_{j+1}(y_1), \ldots, \mathtt{acc}_{j+1}(y_i) &&1 \leq j < 2d, 1 \leq i < N \end{align}\] It is easily verified that the preceding rules behave exactly like \(r_{\mathtt{acc}}, r_{\mathtt{def}}^{i}\) for the first \(2d\) iterations. To make this more formal, let \(\Pi_{\mathtt{arg}}^d\) be the preceding rules. Consider some ABox \(\mathcal{A}\), a priority relation \(\succ\) between facts in \(\mathcal{A}\), and define \(S_{\mathcal{A}, \succ}\) as follows: \[S_{\mathcal{A}, \succ} = \{\gamma \leftarrow \, \mid \gamma \in \mathcal{A}_{id}\} \cup \{ \mathtt{pref}(id(\alpha), id(\beta)) \leftarrow \, \mid \alpha \succ \beta\}\] Now let \(\mathbf{K}_0, \mathbf{K}_1, \ldots\) and \(\mathbf{L}_0, \mathbf{L}_1, \ldots\) be respectively the sequence of instances generated during the computation of the well-founded models of \(\{r_{\mathtt{acc}}\} \cup \{r_{\mathtt{def}}^{i}, 1 \leq i \leq N\} \cup S_{\mathcal{A}, \succ}\) and \(\Pi_{\mathtt{arg}}^d \cup S_{\mathcal{A}, \succ}\) respectively. Then for every \(1 \leq j \leq 2d\), we have the following:

\(\mathtt{acc}_j(\alpha) \in \mathbf{L}_j\) iff \(\mathtt{acc}(\alpha) \in \mathbf{K}_j\)
\(\mathtt{def}_j(\alpha) \in \mathbf{L}_j\) iff \(\mathtt{def}(\alpha) \in \mathbf{K}_j\)

Thus, by combining the \(\Pi_{\mathtt{arg}}^d\) with the program \(\Pi_{\mathtt{confl}}\), we obtain a stratified program whose minimal model contains \(\mathtt{acc}_{2d}(id(\alpha))\) iff \(\alpha \in \Gamma_{F_{\mathcal{K}, \succ}}^d(\emptyset)\). Moreover, by examining the program, we remark that there is no recursion inside the strata of the program. It is known that every non-recursive stratified datalog query can be equivalently expressed as a first-order query, essentially by ‘unfolding’ the rules starting from a chosen goal predicate. We thus obtain:

Theorem 10. For every DL-Lite\(^{\mathcal{H}}_\mathsf{horn}\)TBox \(\mathcal{T}\) and \(d >0\), there exists a first-order query \(\Psi_{\mathcal{T},d}\) with one free variable such that for every ABox \(\mathcal{A}\), priority relation \(\succ\) for \(\mathcal{K}=\langle \mathcal{T}, \mathcal{A}\rangle\), and assertion \(\alpha\), the following are equivalent:

\(\alpha\) belongs to \(\Gamma_{F_{\mathcal{K}, \succ}}^d(\emptyset)\)
\(\Psi_{\mathcal{T},d}(id(\alpha))\) evaluates to true over the finite first-order interpretation corresponding to \(\mathcal{A}_{id} \cup \{ \mathtt{pref}(id(\alpha), id(\beta))\mid \alpha \succ \beta\}\).

Let \(\trianglerighteq\) be a partial preorder (i.e. a reflexive and transitive binary relation) over the ABox \(\mathcal{A}\) of a KB \(\mathcal{K}\). We show that the preferred repair \(\mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq)\) defined in [26] is precisely the intersection of the completion-optimal repairs of \(\mathcal{K}_{\succ_\trianglerighteq}\) where \(\alpha\succ_\trianglerighteq\beta\) iff \(\{\alpha,\beta\}\subseteq C\in\mathit{Conf}(\mathcal{K})\) and \(\alpha\triangleright\beta\) (i.e. \(\alpha\trianglerighteq\beta\) and \(\beta\ntrianglerighteq\alpha\)).

We first recall the definition of \(\mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq)\). Observe that given a total preorder \(\geq\) over \(\mathcal{A}\), \(\succ_\geq\) is score-structured, so the three families of optimal repairs collapse. We denote by \(\mathit{OptRep}(\mathcal{K}, \geq)\) the set \(\mathit{CRep}(\mathcal{K}_{\succ_\geq})=\mathit{GRep}(\mathcal{K}_{\succ_\geq})=\mathit{PRep}(\mathcal{K}_{\succ_\geq})\). The repairs in \(\mathit{OptRep}(\mathcal{K}, \geq)\) correspond to the preferred repairs used in [26], which are the \(\subseteq_P\)-repairs of [17] defined with the priority levels naturally associated with \(\geq\).

Definition 22. Let \(\geq\) be a total preorder that extends \(\trianglerighteq\), i.e. such that for every \(\alpha,\beta\in\mathcal{A}\), if \(\alpha\trianglerighteq\beta\), then \(\alpha\geq \beta\), and if \(\alpha\triangleright\beta\), then \(\alpha> \beta\). The intersection of preferred repairs associated with \((\mathcal{K},\geq)\) is \(\mathit{IPR}(\mathcal{K},\geq) = \bigcap_{\mathcal{A}' \in \mathit{OptRep}(\mathcal{K}, \geq)}\mathcal{A}'\).

The preferred repair associated with \((\mathcal{K},\trianglerighteq)\) is: \(\mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq)= \bigcap_{\geq\text{total extension of }\trianglerighteq} \mathit{IPR}(\mathcal{K},\geq)\).

Theorem 11. For every KB \(\mathcal{K}=\langle \mathcal{T},\mathcal{A}\rangle\) and partial preorder \(\trianglerighteq\) over \(\mathcal{A}\), \(\mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq)=\bigcap_{\mathcal{A}' \in \mathit{CRep}(\mathcal{K}, \succ_\trianglerighteq)}\mathcal{A}'\), where \(\alpha\succ_\trianglerighteq\beta\) iff \(\{\alpha,\beta\}\subseteq C\in\mathit{Conf}(\mathcal{K})\) and \(\alpha\triangleright\beta\).

Proof. Let \(\mathcal{A}^{\cap,C,\succ_\trianglerighteq}=\bigcap_{\mathcal{A}' \in \mathit{CRep}(\mathcal{K}, \succ_\trianglerighteq)}\mathcal{A}'\) be the intersection of the completion-optimal repairs of \(\mathcal{K}_{\succ_\trianglerighteq}\).

Let \(\alpha_0\in \mathcal{A}^{\cap,C,\succ_\trianglerighteq}\), let \(\geq\) be a total preorder that extends \(\trianglerighteq\) and \(\mathcal{A}'\in\mathit{OptRep}(\mathcal{K}, \geq)\). For every \(\alpha,\beta\), if \(\alpha{\succ_\trianglerighteq}\beta\), then \(\{\alpha,\beta\}\subseteq C\in\mathit{Conf}(\mathcal{K})\) and \(\alpha\triangleright\beta\), so since \(\geq\) extends \(\trianglerighteq\), \(\alpha > \beta\), i.e. \(\alpha\succ_\geq\beta\). It follows that \(\succ_\geq\) extends \(\succ_\trianglerighteq\). Hence, the completion-optimal repairs of \(\mathcal{K}_{\succ_\geq}\) form a subset of the completion-optimal repairs of \(\mathcal{K}_{\succ_\trianglerighteq}\), so their intersections are related as follows: \(\bigcap_{\mathcal{A}' \in \mathit{CRep}(\mathcal{K}, \succ_\trianglerighteq)}\mathcal{A}'\subseteq \bigcap_{\mathcal{A}' \in \mathit{CRep}(\mathcal{K}, \succ_\geq)}\mathcal{A}'\). It follows that \(\alpha_0\in \bigcap_{\mathcal{A}' \in \mathit{CRep}(\mathcal{K}, \succ_\geq)}\mathcal{A}'=\bigcap_{\mathcal{A}' \in \mathit{OptRep}(\mathcal{K}, \geq)}\mathcal{A}'=\mathit{IPR}(\mathcal{K},\geq)\). Hence, for every total preorder \(\geq\) that extends \(\trianglerighteq\), \(\alpha_0\in \mathit{IPR}(\mathcal{K},\geq)\). It follows that \(\alpha_0\in \mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq)\). We conclude that \(\mathcal{A}^{\cap,C,\succ_\trianglerighteq}\subseteq \mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq)\).

In the other direction, let \(\alpha_0\in \mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq)\) and let \(\succ'\) be a completion of \(\succ_\trianglerighteq\) and \(\mathcal{A}_{\succ'}\) be the unique optimal repair defined by \(\succ'\). Let \(\geq\) be a total preorder that extends the preorder \(\geq'\) defined as follows: \(\alpha\geq'\beta\) if (i) \(\alpha\trianglerighteq\beta\) or (ii) \(\alpha\succ'\beta\). We show that \(\geq\) extends \(\trianglerighteq\). If \(\alpha\trianglerighteq\beta\) then \(\alpha\geq'\beta\) so \(\alpha\geq\beta\). Assume that \(\alpha\triangleright\beta\). If \(\alpha\) and \(\beta\) are in a conflict, \(\alpha\succ_\trianglerighteq\beta\) so \(\alpha\succ'\beta\) and \(\beta\not\succ'\alpha\) by definition of a completion of a priority relation. If \(\alpha\) and \(\beta\) are not conflicting, \(\beta\not\succ'\alpha\) trivially. Since \(\beta\not\trianglerighteq\alpha\) and \(\beta\not\succ'\alpha\), it follows that \(\beta\not\geq'\alpha\). Hence \(\alpha>'\beta\), so \(\alpha>\beta\) since \(\geq\) extends \(\geq'\). It follows that \(\geq\) extends \(\trianglerighteq\). Thus \(\alpha_0\in\mathit{IPR}(\mathcal{K},\geq)\). We show that \(\mathcal{A}_{\succ'}\in \mathit{OptRep}(\mathcal{K}, \geq)\), which implies that \(\mathit{IPR}(\mathcal{K},\geq)\subseteq\mathcal{A}_{\succ'}\), so that \(\alpha_0\in\mathcal{A}_{\succ'}\). Since \(\mathit{OptRep}(\mathcal{K}, \geq)=\mathit{CRep}(\mathcal{K}_{\succ_\geq})\), it is sufficient to show that \(\succ'\) is a completion of \(\succ_\geq\). Let \(\alpha\succ_\geq\beta\). By definition of \(\succ_\geq\), \(\alpha\) and \(\beta\) are in a conflict and \(\alpha>\beta\). Since \(\succ'\) is a total priority relation and \(\alpha\), \(\beta\) are in a conflict, it must be the case that \(\alpha\succ'\beta\) or \(\beta\succ'\alpha\). However, \(\beta\not\succ'\alpha\). Indeed, otherwise \(\beta\geq'\alpha\) by construction of \(\geq'\), and since \(\geq\) extends \(\geq'\), it follows that \(\beta\geq\alpha\), contradicting \(\alpha>\beta\). Hence \(\alpha\succ'\beta\). It follows that \(\succ'\) is indeed a completion of \(\succ_\geq\), so that \(\alpha_0\in\mathcal{A}_{\succ'}\). We conclude that \(\mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq) \subseteq \mathcal{A}^{\cap,C,\succ_\trianglerighteq}\). ◻

References↩︎

[1]

Poggi, A.; Lembo, D.; Calvanese, D.; De Giacomo, G.; Lenzerini, M.; and Rosati, R. 2008. Linking data to ontologies. Journal of Data Semantics 10:133–173.

[2]

Bienvenu, M., and Ortiz, M. 2015. Ontology-mediated query answering with data-tractable description logics. In Reasoning Web.

[3]

Xiao, G.; Calvanese, D.; Kontchakov, R.; Lembo, D.; Poggi, A.; Rosati, R.; and Zakharyaschev, M. 2018. Ontology-based data access: A survey. In IJCAI.

[4]

Baader, F.; Horrocks, I.; Lutz, C.; and Sattler, U. 2017. An Introduction to Description Logic. Cambridge University Press.

[5]

OWL Working Group, W. 2009. OWL 2 Web Ontology Language: Document overview. W3C Recommendation. Available at https://www.w3.org/TR/owl2-overview/.

[6]

Calvanese, D.; De Giacomo, G.; Lembo, D.; Lenzerini, M.; and Rosati, R. 2007. Tractable reasoning and efficient query answering in description logics: The DL-Lite family. J. Autom. Reasoning 39(3):385–429.

[7]

Artale, A.; Calvanese, D.; Kontchakov, R.; and Zakharyaschev, M. 2009. The DL-Lite family and relations. J. Artif. Intell. Res. 36:1–69.

[8]

Motik, B.; Cuenca Grau, B.; Horrocks, I.; Wu, Z.; Fokoue, A.; and Lutz, C. 2012. 2 Web Ontology Language profiles. ecommendation. Available at http://www.w3.org/TR/owl2-profiles/.

[9]

Bienvenu, M., and Bourgaux, C. 2016. Inconsistency-tolerant querying of description logic knowledge bases. In Reasoning Web.

[10]

Bienvenu, M. 2019. Inconsistency handling in ontology-mediated query answering: A progress report. In DL.

[11]

Lembo, D.; Lenzerini, M.; Rosati, R.; Ruzzi, M.; and Savo, D. F. 2010. Inconsistency-tolerant semantics for description logics. In RR.

[12]

Bienvenu, M., and Rosati, R. 2013. Tractable approximations of consistent query answering for robust ontology-based data access. In IJCAI.

[13]

Lembo, D.; Lenzerini, M.; Rosati, R.; Ruzzi, M.; and Savo, D. F. 2015. Inconsistency-tolerant query answering in ontology-based data access. Journal Web Sem. 33:3–29.

[14]

Bienvenu, M.; Bourgaux, C.; and Goasdoué, F. 2019. Computing and explaining query answers over inconsistent DL-Lite knowledge bases. J. Artif. Intell. Res. 64:563–644.

[15]

Tsalapati, E.; Stoilos, G.; Stamou, G. B.; and Koletsos, G. 2016. Efficient query answering over expressive inconsistent description logics. In IJCAI.

[16]

Trivela, D.; Stoilos, G.; and Vassalos, V. 2018. A framework and positive results for IAR-answering. In AAAI.

[17]

Bienvenu, M.; Bourgaux, C.; and Goasdoué, F. 2014. Querying inconsistent description logic knowledge bases under preferred repair semantics. In AAAI.

[18]

Staworko, S.; Chomicki, J.; and Marcinkowski, J. 2012. Prioritized repairing and consistent query answering in relational databases. Ann. Math. Artif. Intell. 64(2-3):209–246.

[19]

Fagin, R.; Kimelfeld, B.; Reiss, F.; and Vansummeren, S. 2016. Declarative cleaning of inconsistencies in information extraction. ACM Trans. Database Syst. 41(1):6:1–6:44.

[20]

Fagin, R.; Kimelfeld, B.; and Kolaitis, P. G. 2015. Dichotomies in the complexity of preferred repairs. In PODS.

[21]

Kimelfeld, B.; Livshits, E.; and Peterfreund, L. 2017. Detecting ambiguity in prioritized database repairing. In ICDT.

[22]

Livshits, E., and Kimelfeld, B. 2017. Counting and enumerating (preferred) database repairs. In PODS.

[23]

Kaci, S.; van der Torre, L. W. N.; and Villata, S. 2018. Preference in abstract argumentation. In COMMA.

[24]

Flouris, G., and Bikakis, A. 2019. A comprehensive study of argumentation frameworks with sets of attacking arguments. Int. J. Approx. Reasoning 109:55–86.

[25]

Belabbes, S.; Benferhat, S.; and Chomicki, J. 2019. Elect: An inconsistency handling approach for partially preordered lightweight ontologies. In LPNMR.

[26]

Belabbes, S., and Benferhat, S. 2019. Inconsistency handling for partially preordered ontologies: Going beyond Elect. In KSEM.

[27]

Martinez, M. V.; Parisi, F.; Pugliese, A.; Simari, G. I.; and Subrahmanian, V. S. 2014. Policy-based inconsistency management in relational databases. Int. J. Approx. Reason. 55(2):501–528.

[28]

Tanon, T. P.; Bourgaux, C.; and Suchanek, F. M. 2019. Learning how to correct a knowledge base from the edit history. In WWW.

[29]

Bourgaux, C. 2016. Inconsistency Handling in Ontology-Mediated Query Answering. Ph.D. Dissertation, University of Paris-Saclay, France.

[30]

Johnson, D. S.; Papadimitriou, C. H.; and Yannakakis, M. 1988. On generating all maximal independent sets. Inf. Process. Lett. 27(3):119–123.

[31]

Eiter, T., and Gottlob, G. 1995. Identifying the minimal transversals of a hypergraph and related problems. SIAM J. Comput. 24(6):1278–1304.

[32]

Boros, E.; Elbassioni, K. M.; Gurvich, V.; and Khachiyan, L. 2000. An efficient incremental algorithm for generating all maximal independent sets in hypergraphs of bounded dimension. Parallel Processing Letters 10(4):253–266.

[33]

Dung, P. M. 1995. On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artif. Intell. 77(2):321–358.

[34]

Coste-Marquis, S.; Devred, C.; and Marquis, P. 2005. Symmetric argumentation frameworks. In ECSQARU.

[35]

Amgoud, L., and Cayrol, C. 2002. Inferring from inconsistency in preference-based argumentation frameworks. J. Autom. Reasoning 29(2):125–169.

[36]

Amgoud, L., and Vesic, S. 2014. Rich preference-based argumentation frameworks. Int. J. Approx. Reasoning 55(2):585–606.

[37]

Kaci, S.; van der Torre, L. W. N.; and Weydert, E. 2006. Acyclic argumentation: Attack = conflict + preference. In ECAI.

[38]

Nielsen, S. H., and Parsons, S. 2006. A generalization of Dung’s abstract framework for argumentation: Arguing with sets of attacking arguments. In ArgMAS.

[39]

Diller, M.; Keshavarzi Zafarghandi, A.; Linsbichler, T.; and Woltran, S. 2020. Investigating subclasses of abstract dialectical frameworks. Argument & Computation. To appear.

[40]

Croitoru, M., and Vesic, S. 2013. What can argumentation do for inconsistent ontology query answering? In SUM.

[41]

Rao, P.; Sagonas, K.; Swift, T.; Warren, D. S.; and Freire, J. 1997. system for effciently computing WFS. In LPNMR.

[42]

Lopatenko, A., and Bertossi, L. E. 2007. Complexity of consistent query answering in databases under cardinality-based and incremental repair semantics. In ICDT.

[43]

Du, J.; Qi, G.; and Shen, Y. 2013. Weight-based consistent query answering over inconsistent SHIQ knowledge bases. Knowl. Inf. Syst. 34(2):335–371.

[44]

Baget, J.; Benferhat, S.; Bouraoui, Z.; Croitoru, M.; Mugnier, M.; Papini, O.; Rocher, S.; and Tabia, K. 2016. Inconsistency-tolerant query answering: Rationality properties and computational complexity analysis. In JELIA.

[45]

Lukasiewicz, T.; Malizia, E.; and Vaicenavicius, A. 2019. Complexity of inconsistency-tolerant query answering in Datalog+/- under cardinality-based repairs. In AAAI.

[46]

Benferhat, S.; Bouraoui, Z.; and Tabia, K. 2015. How to select one preferred assertional-based repair from inconsistent and prioritized DL-Lite knowledge bases? In IJCAI.

[47]

Gorogiannis, N., and Hunter, A. 2011. Instantiating abstract argumentation with classical logic arguments: Postulates and properties. Artif. Intell. 175(9-10):1479–1497.

[48]

Croitoru, M.; Thomopoulos, R.; and Vesic, S. 2015. Introducing preference-based argumentation to inconsistent ontological knowledge bases. In PRIMA.

[49]

Dvorák, W., and Dunne, P. E. 2017. Computational problems in formal argumentation and their complexity. FLAP 4(8).

[50]

Abiteboul, S.; Hull, R.; and Vianu, V. 1995. Foundations of Databases. Addison-Wesley.

This construction in [50] was originally defined for 3-valued instances, but as is noted there, only 2-valued instances are needed for the fixpoint construction of the well-founded semantics. Focusing on 2-valued instances simplifies some definitions.↩︎

Querying and Repairing Inconsistent Prioritized Knowledge Bases:
Complexity Analysis and Links with Abstract Argumentation

Abstract

1 Introduction↩︎

2 Preliminaries↩︎

3 Querying Inconsistent Prioritized KBs↩︎

4 Complexity Analysis↩︎

4.1 Overview↩︎

4.2 Query Entailment↩︎

4.3 Uniqueness and Enumeration↩︎

4.4 Case of Transitive Priority Relations↩︎

5 Preference-Based Argumentation↩︎

5.1 Argumentation Frameworks↩︎

5.2 Enriching AFs with Preferences↩︎

5.3 Set-Based Argumentation Frameworks↩︎

5.4 Adding Preferences to SETAFs↩︎

6 Linking Prioritized KBs and PSETAFs↩︎

6.1 Optimal Repairs vs. PSETAF Extensions↩︎

6.2 Grounded Semantics for Prioritized KBs↩︎

8 Conclusion and Future Work↩︎

Acknowledgements↩︎

9 Proofs for Section 4 ↩︎

10 Proofs for Section 5 ↩︎

11 Proofs for Section 6 ↩︎

References↩︎

Subjects

Updated on Academus

Querying and Repairing Inconsistent Prioritized Knowledge Bases: Complexity Analysis and Links with Abstract Argumentation

Abstract

1 Introduction↩︎

2 Preliminaries↩︎

3 Querying Inconsistent Prioritized KBs↩︎

4 Complexity Analysis↩︎

4.1 Overview↩︎

4.2 Query Entailment↩︎

4.3 Uniqueness and Enumeration↩︎

4.4 Case of Transitive Priority Relations↩︎

5 Preference-Based Argumentation↩︎

5.1 Argumentation Frameworks↩︎

5.2 Enriching AFs with Preferences↩︎

5.3 Set-Based Argumentation Frameworks↩︎

5.4 Adding Preferences to SETAFs↩︎

6 Linking Prioritized KBs and PSETAFs↩︎

6.1 Optimal Repairs vs. PSETAF Extensions↩︎

6.2 Grounded Semantics for Prioritized KBs↩︎

7 Related Work↩︎

8 Conclusion and Future Work↩︎

Acknowledgements↩︎

9 Proofs for Section 4↩︎

10 Proofs for Section 5↩︎

11 Proofs for Section 6↩︎

12 Comparison with Related Work↩︎

References↩︎

Subjects

Updated on Academus

Querying and Repairing Inconsistent Prioritized Knowledge Bases:
Complexity Analysis and Links with Abstract Argumentation

9 Proofs for Section 4 ↩︎

10 Proofs for Section 5 ↩︎

11 Proofs for Section 6 ↩︎