Description Logic (DL) based ontologies and nonmonotonic rules provide complementary features whose combination is crucial in many applications. In hybrid knowledge bases (KBs), which combine both formalisms, for large real-world applications, often integrating knowledge originating from different sources, inconsistencies can easily occur. These commonly trivialize standard reasoning and prevent us from drawing any meaningful conclusions. When restoring consistency by changing the KB is not possible, paraconsistent reasoning offers an alternative by allowing us to obtain meaningful conclusions from its consistent part. In this paper, we address the problem of efficiently obtaining meaningful conclusions from (possibly inconsistent) hybrid KBs. To this end, we define two paraconsistent semantics for hybrid KBs which, beyond their differentiating properties, are faithful to well-known paraconsistent semantics as well as the non-paraconsistent logic they extend, and tractable if reasoning in the DL component is.
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¸a˜o para a Cieˆncia 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.
Kro¨tzsch et al., 2011], others follow a hybrid combination of ontologies with nonmonotonic rules, either providing a modular approach where rules and ontologies use their own semantics, and allowing limited interaction between them [Eiter et al., 2008], or defining a unifying framework for both components [Motik and Rosati, 2010; Knorr et al., 2011]. Equipped with semantics that are faithful to their constituting parts, these proposals allow for the specification of so-called hybrid knowledge bases (hybrid KBs) either from scratch, benefiting from the added expressivity, or by combining existing ontologies and rule bases.
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
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.1 2
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 :', 9x : ', '1 ^ '2, '1 '2, K ' and not ' also are, 1This work has been published in [Kaminski et al., 2015]. (2) (3) (4) (5) (7) and '1 _ '2, 8x : ', >, 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: KH
KA1; : : : ; KAn; notB1; : : : ; notBm: (1) K H is called the rule head, and the sets fK Aig and fnot Bj g 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.
HasCertif iedSender v :IsM onitored
KIsM onitored(g)
Krisk(g): Krisk(g)
notisLabelled(g): KisLabelled(g)
notrisk(g): KresolvedRisk(g)
KIsM onitored(g): (6)
KHasCertif iedSender(g) (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 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 = f (O)g [ f j K 2 Sg. 3
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 interpretations2 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 = hI; I1i 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 = hM; N i and N = hM1; N1i 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): (hI; I1i; M; N )(P (s)) = 8 b <
t : f iff sI 2 P I ; sI1 2 P I1 iff sI 2 P I ; sI1 62 P I1 iff sI 62 P I ; sI1 62 P I1 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.
2In 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. u uf t f b b t f uf u
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. Definition 5. For two 5- or 6-pairs (M1; N1) and (M2; N2), (M1; N1) k (M2; N2) iff M1 M2 and N1 N2.
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
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 F IVE (Fig. 1) extends the well-known lattice F OU R, 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 F IVE is shown in Fig. 2 and, in the following, we will give intuitions and necessary notions. First, : behaves for all values in F OU R 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 fb; t; f ; ug, 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 (I; M; N )(:') = (I; M; N )(K') = 8 b >< t
f >: u 8 b >>> t < f >> uf >: u iff (I; M; N )(') = b iff (I; M; N )(') 2 ff ; uf g iff (I; M; N )(') = t iff (I; M; N )(') = u iff TM (') = b iff TM (') = t iff TN (') = f iff TM (') = f and TN (') = b otherwise (I; M; N )('1 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 9x : ' 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 = hIi; Ii0i, we can define T M = hT Ii; T Ii0i, and it can be shown that T M is indeed also a p-interpretation. In addition, we abbreviate (TJ 2X J ; hM; N i; hM1; N1i)(') for any ', M , N , M1, and N1, and X 2 fM; N; M1; N1g, with TX (').
Regarding the actual evaluation, K ' being b can be seen as a special case of being t in the sense that no J 2 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 ) j=5 ', if and only if (I; hM; N i; hM; N i)(') 2 fb; tg for each I 2 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 ) j=5 ' and (2) for each 5-pair (M 0; N 0) with M M 0 and N N 0, where at least one of the inclusions is proper, there is I0 2 M 0 such that (I0; hM 0; N 0i; hM; N i)(') 62 fb; tg. 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), K r is t and K iL 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 0; N 0) as described in (2) of Def. 8.
For 5-satisfying (3)-(5), K IM has to be t or b for a) as K r is t, can have any truth value for b) as K r is f , and not be f for c) as K r is u (cf. Fig. 1). However, e.g. any 5-pair mapping K r to f and K IM not to f is not a 5-model since it is not minimal by (2) of Def. 8. Accordingly, K IM 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, K IM and K rR 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 – directly 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 hybrid KB. 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. PGd by transforming each rule of the form (1) into: (a) KH (b) KHd
KA1; : : : ; KAn; notB1d; : : : ; notBmd,
KA1; : : : ; KAn; notB1d; : : : ; notBmd; 3. and the ground doubled hybrid KB KGd = (O; Od; PGd).
We now define a monotonic immediate consequence operator TKGd;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 R d , D d , CKGd;C, and TKGd;C are
KG KG defined on KGd and subsets S and C of kA(KGd) as follows: R d (S)
KG D d (S)
KG
= = = = fKH j PGd contains a rule of the form KH KA1; : : : ; KAn s.t. KAi 2 Sg fK j K 2 kA(KG), obO;S j=5 g[ fK d j K 2 kA(KG), obOd;S j=5 dg fK d j K 2 kA(KG), obO;C j=5 : g (R d (S) [ D d (S)) n CKGd;C(S)
KG KG
Since TKGd;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 K H K A1; : : : ; K An for which there exists a rule of the form (1) in R with KBj 62 S for each 1 j m.
Additionally, let KG = (O; PG) be a ground hybrid KB.
d =S are defined as KG=S = The transforms KG=S and KG (O; PG=S) and KGd=S = (O; Od; PGd=S) respectively.
We can now define an antitonic operator that computes the least fixpoint of TKGd;C w.r.t. the resulting hybrid KB. Definition 12. Let KG be a ground hybrid KB and S kA(KGd). We define the operator d (S) = TKGd=S;S " ! KG and two sequences Pid and Nid as follows.
P0d = ; Pdn+1 = d (Ndn)
Pd! = SKPGd i
N0d = kA(KGd) Ndn+1 = d (Pdn)
Nd! = TKNG id
The sequence of Pid is in fact monotonically increasing, maximizing the set of true and inconsistent non-doubled Katoms, while that of Nid 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 = fI j I j=5 obO;Pd!\kA(KG)g and IN = fI j I j=5 obO;Nd!\kA(KG)g. u cf t f b s b s t f cf u
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 K HCS (and K HCSd), while Nd! = kA(KG d ) n fK IM dg.
Thus, model c) in Ex. 2 is the well-founded 5-model.
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 F IVE (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 F IVE (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 2 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 2 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). 8 b (I; M; N )(:') = <>>> s
t >> f >: u 8 b >>> s >>> t > (I; M; N )(K') = <> f >>> cf > >>> u > : iff (I; M; N )(') = b iff (I; M; N )(') = s iff (I; M; N )(') 2 ff ; cf g iff (I; M; N )(') = t iff (I; M; N )(') = u iff TM (') = b iiiffffff TTTMMM ((('''))) === ftt aas.nnt.dd9TTMNN((('''))) ==6=tff iafnfdTTMN((''))==ffs.t. 6 9M (') = t iff TM (') = f s.t. 9M (') = t and TN (') 6= f (I; M; N )('1
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 9J 2 X (resp. 6 9J 2 X) s.t. (J ; hM; N i; hM1; N1i)(') = y for any ', M , N , M1, and N1, X 2 fM; N; M1; N1g and truth value y, with 9X(') = y (resp. 6 9X(') = 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 ) j=6 ', if and only if (I; hM; N i; hM; N i)(') 2 fb; tg for each I 2 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 ) j=6 K, (2) for every 6-pair (M 0; N 0) with M M 0 and N N 0 where at least one of the inclusions is proper, there is I0 2 M 0 [ N 0 s.t. (I0; hM 0; N 0i; hM; N i)(K) 62 fb; tg, and (3) for every K 2 ( ; hM; N i; hM; N i)(K
kA(KG) it holds that ) 2 fb; cf g if and only if obO;fK 0j( ;hM;Ni;hM;Ni)(K 0)2fb;s;tgg j=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), K IM could also be minimized to cf if K r 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), K IM 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 K r is u, due to the definition of and (3) of Def. 14. In the first case a), K rR can be minimized to s such that support on contradiction can be detected. In the other cases b) and c), K rR is f . Thus, unlike Ex. 2 where K rR 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 K0G;C, where K -atoms whose classical negation is derivable are removed in T K0G;C. Definition 15. Let KG = (O; PG) be a ground positive hybrid KB. The operators RKG , DKG , TKG and T K0G;C are defined on KG and subsets S and C of kA(KG) as follows.
RKG (S) DKG (S)
TKG (S) T K0G;C(S) = fKH j PG contains a rule of the form
KH KA1; : : : ; KAn s.t. KAi 2 Sg = fK j K 2 kA(KG), obO;S j=p g = RKG (S) [ DKG (S) = (RKG (S) [ DKG (S))n
fK j K 2 kA(KG), obO;C j=p : g
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 0KG (S) = T K0G=S;S " ! and two sequences Pi and Ni as follows.
P0 = ; Pn+1 = KG (Nn)
P! = S Pi
N0 = kA(KG) Nn+1 = 0 (Pn)
N! = TKNG i In the alternating fixpoint, KG is used in the sequence of Pi, and 0 in that of Ni. This ensures that K -atoms whose classicKaGl 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 = fI j I j=p obO;P! g and IN = fI j I j=p obO;N! g.
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! = fKHCSg, while N! = fK r; K iLg. Thus, the 6-model c) in Ex. 4 is the well-founded 6-model (where Kr and KiL are u). 4
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 0; N 0) 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 W F SXp [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. W F SXp). Let be an LP with classical negation limited to unary atoms and KG its MKNF-translation. There is a oneto-one correspondence between the well-founded 6-model of KG and the unique well-founded paraconsistent model assigned by W F SXp.
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 .
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 [Dama´sio 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 [Alcaˆntara 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 Prote´ge´ plug-in NoHR [Ivanov et al., 2013] for reasoning with our paraconsistent semantics. Future work also includes investigating Suspicious Reasoning in paraconsistent DLs, both standalone and as parts of hybrid KBs.