Efficient Paraconsistent Reasoning with Ontologies and Rules

1 Introduction

In this paper, we address the problem of dealing with inconsistent knowledge bases consisting of ontologies and nonmonotonic rules, following a paraconsistent reasoning approach with a focus on efficiency.

Description Logics (DLs) and Logic Programs (LPs) provide different strengths when used for Knowledge Representation and Reasoning. While DLs employ the Open World Assumption and are suited for defining ontologies, LPs adopt the Closed World Assumption and are able to express nonmonotonic rules with exceptions and preference orders. Combining features of both formalisms has been actively pursued over the last few years, resulting in different proposals with different levels of integration and complexity: while some extend DLs with rules [Horrocks and Patel-Schneider, 2004;

∗Partially supported by Fundac¸ ˜ao para a Ciˆencia e a Tecnologia under project PTDC/EIA-CCO/121823/2010 and strategic project PEst/UID/CEC/04516/2013. M. Knorr was also supported by grant SFRH/BPD/86970/2012.

The complex interactions between the ontology component and the rule component of these hybrid KBs - even more so when they result from combining existing ontologies and rule bases independently developed - can easily lead to contradictions, which, under classical semantics, trivialize standard reasoning and prevent us from drawing any meaningful conclusions, ultimately rendering these hybrid KBs useless.

One way to deal with this problem is to employ some method based on belief revision (e.g. [Leite, 2003; Osorio and Cuevas, 2007; Slota and Leite, 2012a; 2014; Delgrande et al., 2013] for LPs, [Flouris et al., 2008; Calvanese et al., 2010; Kharlamov et al., 2013] for DLs, and [Slota et al., 2011; Slota and Leite, 2012b] for hybrid KBs) to regain consistency so that standard reasoning services can be used, or some method based on repairing (e.g. [Arenas et al., 1999] for LPs and [Haase et al., 2005] for DLs) where hypothetical belief revision is employed for consistent query answering, without actually changing the KB. However, this is not always feasible e.g. because we may not have permission to change the KB - as for instance in [Alberti et al., 2011] where the KB encodes laws and norms - or because the usual high complexity of belief revision and repairing methods simply renders their application prohibitive. When these methods are not possible or not feasible, paraconsistent reasoning services, typically based on some many-valued logics, offer an alternative by being able to draw meaningful conclusions in the presence of contradiction. Whereas paraconsistent reasoning has been extensively studied in the context of each individual component of hybrid KBs (see Related Work in Sect. 5), it is still a rather unexplored field in the context of hybrid KBs. Notable exceptions are [Huang et al., 2011; 2014; Fink, 2012], yet their computation is not tractable in general even if reasoning in the DL component is.

In this paper, we investigate efficient paraconsistent semantics for hybrid KBs. We adopt the base framework of [Motik and Rosati, 2010] because of its generality and tight integration between the ontology and the rules - c.f. [Motik and Rosati, 2010] for a thorough discussion - under the semantics of [Knorr et al., 2011] because of its computational properties. We extend such semantics with additional truth values to evaluate contradictory pieces of knowledge, following two common views on how to deal with contradictory knowledge bases. According to one view, contradictions are dealt with locally, in a minimally intrusive way, such that a new truth value is introduced to model inconsistencies, while consistent pieces of information whose derivation depends on inconsistent information are still considered to be true in the classical sense. This view is adopted in paraconsistent semantics for DLs, e.g. [Maier et al., 2013], LPs, e.g. [Sakama, 1992; Sakama and Inoue, 1995], and hybrid KBs [Huang et al., 2011; Fink, 2012]. The alternative view is to distinguish truth which depends on the inconsistent part of a KB, from truth which is derivable without involving any contradictory knowledge. This view, commonly referred to as Suspicious Reasoning, is adopted in paraconsistent semantics for LPs, e.g. [Alferes et al., 1995; Sakama, 1992; Sakama and Inoue, 1995] and hybrid KBs [Huang et al., 2014].

We present solutions following both views through the definition of a five-valued and a six-valued paraconsistent semantics for hybrid KBs, the latter implementing Suspicious Reasoning, both of which enjoy the following properties:

• Soundness w.r.t. the three-valued semantics for consistent hybrid KBs by [Knorr et al., 2011];
• Faithfulness w.r.t. semantics for its base formalisms;
• Computability by means of a sound and complete fixpoint algorithm;
• Tractability when a tractable DL is used for the ontology.

The paper is organized as follows: in Sect. 2, we present the formal background; in Sect. 3, we present both semantics, starting with common parts, and proceeding with the fivevalued semantics in Sect. 3.1, and the six-valued one in Sect. 3.2; in Sect. 4, we investigate the properties of both semantics and discuss related work and conclude in Sect. 5.

2 Preliminaries

In this section, we introduce hybrid knowledge bases, and also recall the syntax of MKNF formulas, originating from the logic of minimal knowledge and negation as failure (MKNF) [Lifschitz, 1991], into which the former are embedded. For reasons of space, some details, e.g., on DLs or the semantics for MKNF formulas, are omitted here. These can still be found in [Knorr et al., 2011].

The syntax of MKNF formulas is defined over a functionfree first-order signature Σ = (Σc,Σp), where the sets Σc and Σp contain, resp., all constants and all predicates including the binary equality predicate ≈. Given a predicate P and terms s over Σc and a set of variables, an atom P(s) is an MKNF formula. If ϕ, ϕ1 and ϕ2 are MKNF formulas, then ¬ϕ, ∃x : ϕ, ϕ1 ∧ ϕ2, ϕ1 ⊃ ϕ2, Kϕ and notϕ also are, and ϕ1 ∨ ϕ2, ∀x : ϕ, ⊤, and ⊥ represent the usual syntactic short-cuts. Replacing free variables x in ϕ by terms s is represented by ϕ[s/x]. A closed MKNF formula contains no free variables. Formulas of the form Kϕ and notϕ are called, resp., K-atoms and not-atoms. Intuitively, Kϕ asks if ϕ is known, while notϕ checks if ϕ does not hold, which allows one to draw conclusions from the absence of information.

Hybrid KBs combine a set of MKNF rules and a DL ontology O, which is translatable into a function-free first order formula with equality π(O) and for which checking of satisfiability and instances are decidable [Baader et al., 2003]. An MKNF rule r is of the given form where H, Ai, Bi are atoms:

K H is called the rule head, and the sets {K Ai} and {notBj} are called the positive body and the negative body, respectively. A rule r is positive if m = 0, and r is a fact if n = m = 0. A program P is a finite set of MKNF rules, and positive if all rules in it are positive. A hybrid knowledge base (hybrid KB) K is a pair (O, P). Given such K = (O, P), KG = (O, PG) is a ground hybrid KB where PG denotes the grounding of P using all constants occurring in K as usual. As hybrid KBs can be translated into MKNF formulas using π(O) and the match between → and ⊃ for the MKNF rules, their semantics is derived from that of MKNF formulas, and we abuse notation and refer to such translation π(K) by K. To achieve decidability of reasoning, hybrid KBs are restricted to be DL-safe, basically requiring that variables in rules appear at least once in the positive body under a predicate which does not occur in O, thus limiting the applicability of constants in rules to those in P. From now on, we only consider DL-safe hybrid KBs as it can always be ensured [Ivanov et al., 2013].

Example 1. Consider the following simplified ground hybrid KB KG for assessing the risk of goods at a port.

(4) and (5) state that good g is either a risk (r) or it is labeled (iL). Any risk is monitored (IM) (3), thus a resolved risk (rR) (6). As g has a certified sender (HCS) (7), it can be proven by means of axiom (2) that it is not monitored. Thus, g can be derived to be monitored and not monitored at the same time if it is considered to be a risk, which can only be modeled by means of a paraconsistent evaluation.

Let KG = (O, PG) be a ground hybrid KB. The set of Katoms of KG, written kA(KG), is the smallest set that contains (i) all ground K-atoms occurring in PG, and (ii) a K-atom Kξ for each not-atom notξ occurring in PG. For a subset S of kA(KG), the objective knowledge of S w.r.t. KG is the set of first-order formulas obO,S = {π(O)}∪{ξ | Kξ ∈ S}.

3 Paraconsistent MKNF Semantics

In this section, we define two paraconsistent semantics for hybrid KBs, namely 5- and 6-models, their main difference being whether Suspicious Reasoning is supported in the rules of the hybrid KB or not. This requires the integration of different concepts and assumptions w.r.t. paraconsistency, independently developed for each of the base formalisms. E.g. Suspicious Reasoning has not been considered in DLs, so developing a unified semantics that is faithful to the paraconsistent semantics of the two base formalisms, thus limiting Suspicious Reasoning to inconsistencies from the LP, is highly non-trivial. Finding a model theory corresponding to some LP fixed-point based semantics is also very challenging. All this while maintaining faithfulness to the three-valued semantics [Knorr et al., 2011], including properties such as Coherence, i.e. false (first-order) formulas are also default false. We start with common notions of both semantics.

First, we introduce p-interpretations, which extend firstorder interpretations 1 with the ability to represent that certain pieces of information are true and false at the same time.

Definition 1. Given two first-order interpretations I and I1 with I1 ⊆ I, the pair I = 〈I, I1〉 is called a p-interpretation.

Intuitively, I indicates what is true (t) and false (f), while the additional interpretation I1 only designates for each (true) element in I if it is actually inconsistent (b - for both) or not. No fourth value is assigned, arguably resulting in a simpler paraconsistent semantics for first-order formulas, and at the same time in a stronger consequence relation [Priest, 1979].

P-interpretations are the basis for defining structures used in both semantics, subsequently defined, for interpreting MKNF formulas, to which hybrid KBs can be translated.

Definition 2. A 6-structure (I,M,N) consists of a pinterpretation I and two pairs M = 〈M,N〉 and N = 〈M1,N1〉 of sets of p-interpretations. A 5-structure is a 6structure where M1 ⊆ M and N1 ⊆ N.

Thus, a 5-structure is a special case of a 6-structure.

As common with MKNF semantics, M and N will be used, resp., to evaluate K- and not-atoms, while the pinterpretation I is used to evaluate first-order expressions. In particular, the latter applies in both semantics to atoms, according to the intuition given after Def. 1.

Definition 3. Given 5- or 6-structure (I,M, N), atom P(s):

The evaluation of complex MKNF formulas differs for 5- and 6-structures, and is therefore spelled out separately.

Also based on p-interpretations are the notions that represent potential model candidates for each of the semantics.

Definition 4. A 6-pair (M,N) consists of two non-empty sets M, N of p-interpretations. A 5-pair (M,N) is a 6-pair where N ⊆M. If M = N, then (M,N) is called total.

1 In MKNF semantics, commonly the standard name assumption (SNA) is imposed on interpretations I, i.e., (1) the universe ∆ of I contains Σc and an infinite supply of additional constants, (2) constants are mapped to themselves, and (3) equality is interpreted as a congruence relation. As first-order consequences under SNA and the standard first-order semantics are not distinguishable [Motik and Rosati, 2010], we also assume SNA here and in the remainder.

It is possible to define a so-called knowledge order ⪰k on 5-pairs and 6-pairs, with the intuition that elements which are greater allow one to derive more true and false knowledge.

Some 5- and 6-pairs will turn out to be 5- and 6-models as defined next in Sects. 3.1 and 3.2, and the order ⪰k will be used to compare such 5- and 6-models, and single out those that are most skeptical.

Definition 6. Let ϕ be a closed MKNF formula and (M,N) a 5-model (6-model) of ϕ such that (M1,N1) ⪰k (M,N) for all 5-models (6-models) (M1,N1) of ϕ. Then (M,N) is a well-founded 5-model (well-founded 6-model) of ϕ.

In Sects. 3.1 and 3.2, we will now provide a model-based account of 5- and 6-models and a procedural characterization of the (unique) well-founded 5- and 6-model.

3.1 Five-Valued Semantics

We begin with the five-valued semantics, whose motivation stems from the fact that, for the three-valued MKNF semantics [Knorr et al., 2011], with truth values true, false and undefined (t, f and u resp.), two kinds of inconsistencies are identified. Namely, either some piece of information is simultaneously considered true and false, or undefined and false. We handle this by introducing for each of the two cases a further truth value, namely inconsistent (b) and undefined false (uf), respectively. The resulting lattice FIVE (Fig. 1) extends the well-known lattice FOUR, and is not symmetric simply because no inconsistencies can occur between t and u in [Knorr et al., 2011], as t always prevails in this case.

The evaluation of closed MKNF formulas in 5-structures for the truth values in FIVE is shown in Fig. 2 and, in the following, we will give intuitions and necessary notions. First, ¬ behaves for all values in FOUR as expected. The remaining case follows the intuition that uf behaves under negation like f . The implication ⊃ is defined (Fig. 1) like internal implication by [Maier et al., 2013] for {b, t, f, u}, apart from the case u ⊃ f , which is no longer mapped to t, as it does correspond to the kind of inconsistency between u and f in [Knorr et al., 2011], for which we introduced uf in the first place. Hence, u ⊃ uf is mapped to t, which also corresponds to the idea that uf behaves under ⊃ like a special case of u.

For ∧ and ∨, min and max are used like in [Knorr et al., 2011] instead of the join and meet operations, more common for paraconsistent semantics, and this originates from the fact that b and uf should behave like special cases of t and u respectively, that are only necessary if there is an explicit occurrence of an inconsistency. This means that, if a rule body

Figure 2: Recursive five-valued evaluation of a closed MKNF formula in a 5-structure (I,M, N), given that ϕ, ϕ1, and ϕ2 are MKNF formulas, and that M = 〈M, N〉 and N = 〈M1, N1〉. The operator ⊃ is evaluated as shown in Fig. 1. The operators ∧ and ∨ are defined respectively as min and max on the order f < u < uf < t < b.

is b, then its head should be t, unless we can explicitly derive the negation of the head elsewhere, and similarly for a rule body that is uf whose head should be u, unless we can explicitly derive its negation (or alternatively that it is t or b which would prevail over the derivation from this rule). Thus, the order f < u < uf < t < b implicitly reduces to f < u < t in [Knorr et al., 2011]. This means that if a rule body contains (a conjunction of) two elements that are b and u, then the head is u from this rule alone, and not f , and, for ∨, that ∃x : ϕ should be t if there is one replacement of x which makes it b, one that is u (or uf), and none that is t.

For the evaluation of K and not, we employ intersections over sets of p-interpretations present in 5- and 6structures for which we introduce specific notation. Namely, we can intersect p-interpretations component-wise to obtain the pieces of information on which they coincide. Given a set M of p-interpretations Ii = 〈Ii, I ′ i 〉, we can define ⋂ M = 〈⋂ Ii, ⋂ I ′ i 〉, and it can be shown that ⋂ M is indeed also a p-interpretation. In addition, we abbreviate (⋂J∈X J , 〈M,N〉, 〈M1,N1〉)(ϕ) for any ϕ, M, N, M1, and N1, and X ∈ {M, N, M1, N1}, with ⋂X (ϕ).

Regarding the actual evaluation, Kϕ being b can be seen as a special case of being t in the sense that no J ∈ M can map ϕ to t, and likewise for uf and u w.r.t. M1, i.e. uf behaves like (a special case of) u. The evaluation of notϕ is symmetric to that of Kϕ, for all but uf , which, again, behaves under negation like f . Using intersections in this evaluation slightly deviates, formally, from [Knorr et al., 2011], but the differences are of no impact for hybrid KBs, and this choice results in a simpler notation.

With the evaluation in 5-structures in place, we can define 5-satisfaction for 5-pairs as follows.

Definition 7. Given a closed MKNF formula ϕ, a 5-pair (M,N) 5-satisfies ϕ, written (M,N) |=5 ϕ, if and only if (I, 〈M, N〉, 〈M, N〉)(ϕ) ∈ {b, t} for each I ∈ M.

For defining 5-models, an additional preference order over 5-pairs is required, minimizing knowledge under operator K.

Definition 8. Any 5-pair (M,N) is a 5-model for a given closed MKNF formula ϕ iff

1. (M,N) |=5 ϕ and
2. for each 5-pair (M ′ ,N ′ ) with M ⊆ M ′ and N ⊆ N ′ , where at least one of the inclusions is proper, there is

I ′ ∈M ′ such that (I ′ , 〈M ′ ,N ′ 〉, 〈M,N〉)(ϕ) ̸∈ {b, t}. If ϕ has a 5-model, then ϕ is 5-consistent.

The evaluation of not-atoms is fixed before checking whether M and N are maximal, i.e. whether the evaluation of Katoms is minimal w.r.t. the order f < u < uf < t < b.

Example 2. Consider KG from Ex. 1. For (4) and (5) alone, there are three 5-models since it is not determined whether g is labelled or a risk: a), Kr is t and KiL is f , b), vice-versa, or c), both are u. Both being b would also 5-satisfy (4) and (5), but with the evaluation of not-atoms fixed to b in such a 5-pair (M,N), the rule heads can be t to satisfy the rules, and there is (M ′ ,N ′ ) as described in (2) of Def. 8.

For 5-satisfying (3)-(5), KIM has to be t or b for a) as Kr is t, can have any truth value for b) as Kr is f , and not be f for c) as Kr is u (cf. Fig. 1). However, e.g. any 5-pair mapping Kr to f and KIM not to f is not a 5-model since it is not minimal by (2) of Def. 8. Accordingly, KIM is minimized to t for a), to f for b), and to u for c).

Taking all of KG, there is a conflict between (2) and (3) if Kr is t (model a)) or u (model c)) since the classical negation of IM is also derivable. Thus, for the three possible 5-models for (4) and (5) alone, KIM and KrR are resp. minimized to b and t for model a), to f and f for model b), and to uf and u for c). Note that the head of (6) is evaluated as if the body was t and u respectively, w.r.t. models a) and c). Hence, neither kind of inconsistency is propagated, i.e., for a), KIM is b, yet KrR is t, and for c) KIM is uf , yet KrR is u.

As reasoning - entailment from hybrid KBs - with models that are usually infinite would be unfeasible, we adopt a common technique for reasoning with hybrid KBs [Motik and Rosati, 2010; Knorr et al., 2011] and provide a finite representation of 5-models and the well-founded 5-model in particular, which can be directly used for query answering w.r.t. entailed information. Similarly to [Knorr et al., 2011], this finite representation is obtained via a fixpoint construction.

To introduce this fixpoint construction for the five-valued semantics, we first define a variant of the doubling of hybrid KBs in [Alferes et al., 2013], for which we introduce a new predicate Ad for each predicate A appearing in KG. Here, we abuse notation and denote also with Ad the atom resulting from replacing the original predicate A with Ad . It will be clear from the context whether Ad is a predicate or an atom.

Definition 9. Let KG = (O,PG) be a ground hybridKB. We introduce a new predicate Ad for each predicate A appearing in KG, and we constructively define

1. Od by substituting each predicate A in O by Ad ;
2. P dG by transforming each rule of the form (1) into:
3. (a) KH ←KA1, . . . ,KAn, notBd 1 , . . . , notBdm,
4. (b) KHd ←KA1, . . . ,KAn, notBd 1 , . . . , notBdm;
5. and the ground doubled hybrid KB KdG = (O,Od ,P dG).

We now define a monotonic immediate consequence operator TKdG,C. It collects the consequences from the program component and from the ontology, and subtracts those doubled K-atoms of which the classical negation is derivable.

Definition 10. Let KG = (O, PG) be a ground positive hybrid KB. The operators RKdG , DKdG , CKdG,C, and TKdG,C are defined on KdG and subsets S and C of kA(KdG) as follows:

Since TKdG,C is only defined for positive hybrid KBs, a standard transformation for general hybrid KBs is introduced.

Definition 11. Let R be a set of ground MKNF rules and S a set of ground K-atoms. The transform R/S contains all rules KH ←KA1, . . . ,KAn for which there exists a rule of the form (1) in R with KBj ̸∈ S for each 1 ≤ j ≤ m.

Additionally, let KG = (O,PG) be a ground hybrid KB. The transforms KG/S and KdG/S are defined as KG/S = (O, PG/S) and KdG/S = (O, Od , P dG/S) respectively.

We can now define an antitonic operator that computes the least fixpoint of TKdG,C w.r.t. the resulting hybrid KB.

Definition 12. Let KG be a ground hybrid KB and S ⊆ kA(KdG). We define the operator ΓKdG (S) = TKdG/S,S ↑ ω and two sequences Pdi and Ndi as follows.

The sequence of Pdi is in fact monotonically increasing, maximizing the set of true and inconsistent non-doubled Katoms, while that of Ndi is monotonically decreasing, minimizing the set of non-doubled K-atoms that are not false. It can be shown that both sequences are finite, in fact, even of polynomial length, so that both Pdω and Ndω exist for every ground hybrid KB and are unique.

Theorem 1 (Soundness and completeness). Let KG be a 5-consistent, ground hybrid KB, and Pdω and Ndω the fixpoints of the corresponding sequences. Then (IP , IN) is the well-founded 5-model of KG, where IP = {I | I |=5 obO,Pdω ∩kA(KG)} and IN = {I | I |=5 obO,Ndω ∩kA(KG)}.

By Theorem 1, Pdω and Ndω constitute a finite representation of the well-founded 5-model and can, for example, be used for query answering w.r.t. entailed information. Hence, by computing the two fixpoints for KG of Example 1, the truth values of all K-atoms appearing in kA(KG) w.r.t. its well-founded 5-model can be determined.

Example 3. Recall KG from Ex. 1. Then, Pdω contains only KHCS (and KHCSd ), while Ndω = kA(KdG) \ {KIM d}. Thus, model c) in Ex. 2 is the well-founded 5-model.

3.2 Six-Valued Semantics

The motivation for the six-valued semantics can be described as extending the five-valued semantics with the capability for Suspicious Reasoning. This results in two important changes. First, in order to implement Suspicious Reasoning, we introduce a further truth value suspicious (s), which will be assigned to K-atoms that are not explicitly inconsistent, i.e. not derivable to be true and false at the same time, but whose truth (in the five-valued semantics) is only derivable from a contradiction in the program (i.e. its derivation depends on an inconsistency in the program). Second, we replace uf with cf (classically false), which will be assigned to K-atoms that are neither t nor b, but whose classical negation is derivable (from the ontology). Differently from uf for the five-valued semantics, cf can be viewed as a special case of f (rather than u), and no further undefined knowledge can be derived from it. Thus, classical falsity of K-atoms is propagated in the semantics. All this results in the lattice SIX (Fig. 3).

The evaluation of closed MKNF formulas in 6-structures for SIX is shown in Fig. 4 and, subsequently, we will again provide intuitions and necessary notions. First, ¬ behaves for values in FIVE (replacing uf by cf) as in the five-valued semantics, and the new value s mirrors the behavior of b.

The implication ⊃ is defined (Fig. 3) for all values in FIVE (again replacing uf by cf) as in the five-valued semantics, only that all non-designated truth values have been mapped to f for simplicity. The only differing case is cf ⊃ f which is now t (while uf ⊃ f is uf in the five-valued semantics). This is justified by the fact that cf is understood as a special case of f in general (and not of u). For, s ⊃ x, s behaves like b for any x ∈ SIX, which is motivated by the idea that the propagation of an inconsistency will itself also be propagated. For x ⊃ s, s behaves like t for all x ∈ SIX but t and u. These two cases are mapped to f , based on the intuition that a consequent of an implication with true (undefined) antecedent does not depend on a contradiction since it is independently derivable to be true (undefined).

Figure 4: Recursive evaluation of an MKNF formula in a 6-structure (I,M, N), given that ϕ, ϕ1, and ϕ2 are MKNF formulas, and that M = 〈M, N〉 and N = 〈M1, N1〉. The operator ⊃ is evaluated as shown in Fig. 3. The operators ∧ and ∨ are defined respectively to be the join and meet operation in the lattice SIX.

For ∧ and ∨, the join and meet operations on SIX are used, which are both standard for paraconsistent semantics.

For the evaluation of the operators K and not, we may refer to the (non-)existence of p-interpretations in sets of them. For readability, we abbreviate ∃J ∈ X (resp. ̸ ∃J ∈ X) s.t. (J , 〈M,N〉, 〈M1,N1〉)(ϕ) = y for any ϕ, M, N, M1, and N1, X ∈ {M, N, M1, N1} and truth value y, with ∃X(ϕ) = y (resp. ̸ ∃X(ϕ) = y).

Regarding the actual evaluation, the observations for K and not from Sec. 3.1 persist. Then, s can be seen as a second special case of t (different from b). The changes w.r.t. the cases for f , cf , and u occur basically because a) for 6-pairs (M, N) N ⊆ M does no longer hold, and b) more importantly, cf is now to be understood as a special case of f and not u.

Since N ⊆ M does not hold for 6-pairs (Def. 4), we have to check all p-interpretations in both M∪N for p-satisfaction. Definition 13. Given a closed MKNF formula ϕ, a 6pair 6-satisfies ϕ, written (M,N) |=6 ϕ, if and only if (I, 〈M, N〉, 〈M, N〉)(ϕ) ∈ {b, t} for each I ∈ M ∪ N.

The definition of a 6-model only applies to hybrid KBs, so we can refer directly to K-atoms in the program in a new third condition ensuring that certain 6-models that contain unjustified evaluations to b or cf are removed.

Definition 14. Let (M,N) be a 6-pair and K = (O,P) a hybrid KB. Any 6-pair (M, N) is a 6-model of K iff

1. (M,N) |=6 K,
2. for every 6-pair (M ′ ,N ′ ) with M ⊆ M ′ and N ⊆ N ′ where at least one of the inclusions is proper, there is I ′ ∈M ′ ∪N ′ s.t. (I ′ , 〈M ′ ,N ′ 〉, 〈M,N〉)(K) ̸∈ {b, t}, and
3. for every K ξ ∈ kA(KG) it holds that (∗, 〈M,N〉, 〈M,N〉)(K ξ) ∈ {b, cf} if and only if obO,{Kξ′ |(∗,〈M,N〉,〈M,N〉)(Kξ′ )∈{b,s,t}} |=6 ¬ξ. If ϕ has a 6-model, then ϕ is 6-consistent.

Example 4. Recall KG (Ex. 1) and the three different evaluations of Kr and KiL in the 5-models a)-c) in Ex. 2. Without axiom (2), KIM could also be minimized to cf if Kr is u (model c)), but this would be prevented by (3) of Def. 14 as ¬IM would not be derivable. Condition (3) also removes all 6-models where KHCS is b, so it has to be t.

With the contradiction from (2), KIM has to be b for a) where Kr is t, and KIM has to be cf for b) if Kr is f or c) where Kr is u, due to the definition of ⊃ and (3) of Def. 14. In the first case a), KrR can be minimized to s such that support on contradiction can be detected. In the other cases b) and c), KrR is f . Thus, unlike Ex. 2 where KrR is u if KIM is uf , the falsity is propagated to KrR if KIM is cf , so no undefined knowledge can be derived from KIM.

As before, we introduce a fixpoint construction which will provide a finite representation of the well-founded 6-model.

We define two operators TKG and T ′KG,C , where K-atoms whose classical negation is derivable are removed in T ′KG,C .

Definition 15. Let KG = (O, PG) be a ground positive hybrid KB. The operators RKG , DKG , TKG and T ′KG,C are defined on KG and subsets S and C of kA(KG) as follows.

Reusing the transform (Def. 11), we define two operators. Definition 16. Let KG = (O,PG) be a ground hybrid KB and S ⊆ kA(KG). We define the two operators ΓKG (S) = TKG/S ↑ ω, and Γ′KG (S) = T ′KG/S,S ↑ ω and two sequences Pi and Ni as follows.

In the alternating fixpoint, ΓKG is used in the sequence of Pi, and Γ′KG in that of Ni. This ensures that K-atoms whose classical negation is derivable are not contained in the latter sequence that minimizes the set of K-atoms that are t or u.

As for the five-valued semantics, the unique well-founded 6-model can be obtained from the fixpoints Pω and Nω.

Theorem 2 (Soundness and completeness). Let KG be a 6consistent, ground hybrid KB, and Pω and Nω the fixpoints of the corresponding sequences. Then (IP , IN) is the wellfounded 6-model of KG, where IP = {I | I |=p obO,Pω } and IN = {I | I |=p obO,Nω }.

So, similar to Theorem 1, Theorem 2 provides the desired finite representation of the well-founded 6-model for a hybrid KB, and, thus, allows to determine the truth values of the atoms in Example 1 w.r.t. its well-founded 6-model.

Example 5. Recall KG from Ex. 1. Then, Pω = {KHCS}, while Nω = {Kr,KiL}. Thus, the 6-model c) in Ex. 4 is the well-founded 6-model (where Kr and KiL are u).

4 Properties

In this section, we show several important properties of our two semantics that demonstrate that both are well-defined.

First, both semantics generalize the three-valued semantics for hybrid KBs [Knorr et al., 2011], in the sense that for each so-called 3-model, a corresponding 5- and 6-model exists.

Theorem 3 (Faithfulness w.r.t. the three-valued MKNF semantics). Let KG = (O,PG) be a ground hybrid KB, and (M, N) a 3-model of KG. Then, there exists a corresponding 5- and 6-model (M ′ , N ′ ) of KG, and both coincide.

This 5- and 6-model can in fact be constructed, yet the converse does not hold, i.e. there are 5- and 6-models of KG without a corresponding 3-model (due to inconsistencies) which is also why no general correspondence on the unique wellfounded models for the three semantics exists.

Both semantics are also faithful w.r.t. ALC4 [Ma et al., 2007], provided that, in ALC4, no gaps are admitted, i.e., no truth value u, as well as ⊤ and ⊥ are represented by short-cuts as shown in [Maier et al., 2013], which is what we assume.

Theorem 4 (Faithfulness w.r.t. ALC4). Let O be an ALC4 ontology. Models of O in ALC4 without gaps are in a bijection with p-interpretations that evaluate π(O) to t or b.

Moreover, the six-valued semantics also covers WFSXp [Alferes et al., 1995], which is defined for LPs with explicit negation and implements Suspicious Reasoning, using a socalled MKNF-translation. Our result applies whenever classical negation in LPs is limited to unary program atoms.

Theorem 5 (Faithfulness of the six-valued semantics w.r.t. WFSXp). Let Π be an LP with classical negation limited to unary atoms and KΠG its MKNF-translation. There is a oneto-one correspondence between the well-founded 6-model of KΠG and the unique well-founded paraconsistent model assigned by WFSXp.

No similar result for the five-valued semantics exists since no corresponding well-founded semantics for LPs exists.

Data complexity of computing the finite representations of the well-founded 5- and 6-models depends on the DL used.

Theorem 6 (Data Complexity). Let K = (O,P) be a hybrid KB where entailment of ground atoms in the DL of O is decidable with data complexity C. Then, computing the fixpoints corresponding to the well-founded 5- and 6-model of K is in P C w.r.t. the data complexity.

Notably, data complexity for paraconsistent reasoning does not increase when compared to [Knorr et al., 2011], and, if the considered DL-fragment is polynomial, then computing the fixpoints is in P.

5 RelatedWork and Conclusions

We have introduced two novel paraconsistent semantics for hybrid KBs. They differ in whether inconsistencies and classical falsity are propagated in the program component of the KB. We have provided faithfulness results for both semantics and have shown that they are efficiently computable if the employed ontology language is tractable.

Paraconsistent reasoning has been extensively studied in both base formalisms of hybrid KBs. For DLs, most work [Patel-Schneider, 1989; Straccia, 1997; Ma et al., 2007; Zhang et al., 2009; Maier et al., 2013] focuses on four-valued semantics, varying which classical rules of inferences they satisfy. The approach to which both our semantics are faithful, [Ma et al., 2007; Maier et al., 2013], is most general as it covers SROIQ, the DL behind OWL 2, considers tractable subclasses and truth value removals, and permits re-using classical reasoners. Also considered are three-valued semantics for DLs [Zhang et al., 2010] and measuring the degree of inconsistency in DL-Lite [Zhou et al., 2012]. For LPs, the survey [Dam´asio and Pereira, 1998] discusses e.g. a four-valued semantics without default negation [Blair and Subrahmanian, 1989], a four-, six-, and nine-valued semantics [Sakama and Inoue, 1995] for answer sets [Gelfond and Lifschitz, 1991], and a seven- [Sakama, 1992] and nine-valued [Alferes et al., 1995] well-founded semantics [Gelder et al., 1991]. Notably, the latter, to which our six-valued semantics is faithful, admits both the Coherence Principle and Suspicious Reasoning. More recently, a very general framework for arbitrary bilattices of truth values [Alcˆantara et al., 2005] and paraconsistent Datalog [de Amo and Pais, 2007] have been considered.

Only two paraconsistent semantics for combinations of DLs and LPs directly relate to ours. Both build on answer sets, so their computation is not tractable even with polynomial DLs, and unlike ours, their first-order semantics is four-valued, resulting in a weaker consequence relation. The first, [Huang et al., 2011], is defined for hybrid KBs in MKNF like ours, but extends [Motik and Rosati, 2010] and is four-valued and faithful to [Sakama and Inoue, 1995; Ma et al., 2007]. A nine-valued extension to cover Suspicious Reasoning is considered in [Huang et al., 2014]. The paraconsistent hybrid semantics [Fink, 2012] is a nine-valued extension of semi-equilibrium semantics [Eiter et al., 2010], and faithful to [Sakama and Inoue, 1995; Maier et al., 2013], but Suspicious Reasoning is not considered.

In the future, our fixpoint computations can be used to adapt the Prot´eg´e plug-in NoHR [Ivanov et al., 2013] to also consider reasoning with our paraconsistent semantics. Future work also includes investigating Suspicious Reasoning in paraconsistent DLs, both standalone and as parts of hybrid KBs.