Three-Valued Semantics for Hybrid MKNF Knowledge Bases Revisited (Extended Abstract)

1 Introduction

Motivated by the Semantic Web and other applications, researchers have studied ways to combine rules with description logics (DLs), and in general with decidable first-order theories or external reasoning sources (e.g., [Bruijn et al., 2007; Eiter et al., 2005; Kaminski et al., 2015; Motik and Rosati, 2007; 2010; Rosati, 2006; Vennekens et al., 2010; Yang et al., 2011]).

Of various approaches, the formalism of hybrid MKNF KBs [Motik and Rosati, 2010] is considered a powerful, dominating knowledge representation language developed for this purpose. A hybrid MKNF KB K consists of two components, K = (O,P), where O is a DL knowledge base and P is a collection of MKNF rules based on the stable model semantics. One critical issue centers around combining open and closed world reasoning for targeted applications. This issue is addressed in [Motik and Rosati, 2010] by seamlessly integrating rules with DLs under two-valued MKNF structures.

∗This paper is an extended abstract of the article [Liu and You, 2017] in Artificial Intelligence, 252: 123-138, 2017.

Knorr et al. [Knorr et al., 2011] formulate a three-valued logic of MKNF, define the notion of well-founded MKNF model as the least defined three-valued MKNF model, and show that, if a hybrid MKNF knowledge base K is MKNFconsistent, i.e., K has at least one three-valued MKNF model, then the well-founded MKNF model for K uniquely exists and can be computed by an alternating fixpoint construction.

In this work, we show that (i) an MKNF-consistent hybrid MKNF knowledge base may have a well-founded MKNF model (as defined in [Knorr et al., 2011]), which cannot be computed by the alternating fixpoint construction; and (ii) an MKNF-consistent hybrid MKNF knowledge base may have three-valued MKNF models none of which is the least defined, since they are not comparable by undefinedness. These insights lead to a classification of hybrid MKNF knowledge bases into a hierarchy, where the innermost subclass is precisely what is intended by the well-founded semantics.

The powerful notion of three-valued MKNF models motivates the question whether there is a simpler, more intuitive notion to express these models. Inspired by the notion of partial stable models in logic programming [Przymusinski, 1990; You and Yuan, 1994], we introduce the notion of stable partitions and show a one-to-one correspondence between them and three-valued MKNF models. We further show that the alternating fixpoint construction has another, somewhat unexpected, proof-theoretic utility: we can guess-and-verify whether a partial partition is stable by computing alternating fixpoints and by performing a consistency test. This algorithm can be applied to compute three-valued MKNF models, as well as two-valued ones. As a result, our work provides a uniform characterization of well-founded, two-valued, and all three-valuedMKNF models in terms of stable partition. It also leads to updated complexity results as well as reasoning tools for deciding three-valued entailment for hybrid MKNF.

2 Three-Valued Formalism for MKNF

The logic of MKNF [Lifschitz, 1991] is proposed by Lifschitz as a unifying framework for nonmonotonic formalisms. MKNF formulas are built from first-order formulas and two modal operators, K and not, for closed world reasoning.

Let Σ = (Σc, Σf , Σp) be a first-order signature, where Σc, Σf , and Σp are sets of constants, function symbols, and predicate symbols containing equality ≈, respectively. A firstorder atom P(t1, . . . , tn) is an MKNF formula, where P is a predicate and ti are first-order terms. If no variables occur in such an atom, it is called ground. If ϕ and ϕ′ are MKNF formula, then ¬ϕ, ∃x : ϕ, Kϕ, notϕ, and ϕ ∧ ϕ′ are MKNF formulas. The symbols ∨, ⊃, ∀ are interpreted as usual.

Let Σ be a signature and ∆ a nonempty set called a universe. A first-order interpretation I over Σ and ∆ is defined as usual, with an additional condition that for each element α ∈ ∆, the signature Σ is required to contain a special constant nα, called a name, such that nIα = α.

An MKNF structure is a triple (I,M,N), where I is a first-order interpretation over ∆ and Σ, and M and N are nonempty sets of first-order interpretations over ∆ and Σ. Given an MKNF structure (I,M,N), two-valued satisfiability of an MKNF formula is defined as follows:

Let ϕ be an MKNF formula. An MKNF interpretation M over a universe ∆ is a nonempty set of first-order interpretations over ∆, and M satisfies ϕ, denoted M |= ϕ, if (I,M,M) |= ϕ for each I ∈ M. An MKNF interpretation M is a two-valued MKNF model of ϕ if (i) M |= ϕ, and (ii) ∀M ′ s.t. M ′ ⊃M, (I ′ ,M ′ ,M) ̸|= ϕ for some I ′ ∈M ′ .

The notion of the MKNF structure is extended to that of three-valued MKNF structure (I,M,N), which consists of a first-order interpretation, I, and two pairs, M = 〈M,M1〉 and N = 〈N, N1〉, of sets of first-order interpretations, where M1 ⊆ M and N1 ⊆ N. From 〈M,M1〉, we can identify three truth values for modal K-atoms in the following way: Kϕ is true w.r.t. 〈M,M1〉 if ϕ is true in all interpretations in M; it is false if it is false in at least one interpretation inM1; and it is undefined otherwise. For not-atoms, a symmetric treatment w.r.t. 〈N,N1〉 is adopted. Let {t, u, f} be the set of truth values true, undefined, and false with the order f < u < t, and let the operator max (resp. min) choose the greatest (resp. the least) element with respect to this ordering. A three-valued MKNF formula is evaluated as follows:

A (three-valued) MKNF interpretation pair (M,N) consists of two MKNF interpretations, M and N, with ∅ ⊂ N ⊆

M. An MKNF interpretation pair satisfies an MKNF formula ϕ, denoted (M,N) |= ϕ, iff (I, 〈M,N〉, 〈M,N〉)(ϕ) = t for each I ∈ M. If M = N, then the MKNF interpretation pair is called total. If there exists an MKNF interpretation pair satisfying a formula ϕ, then ϕ is said to be consistent (or satisfiable); otherwise ϕ is inconsistent.

An MKNF interpretation pair (M,N) is a three-valued MKNF model of an MKNF formula ϕ if (i)(M,N) |= ϕ, and (ii) for all MKNF interpretation pairs (M ′ ,N ′ ) with M ⊆ M ′ and N ⊆ N ′ , where at least one of the inclusions is proper and M ′ = N ′ if M = N, ∃I ′ ∈ M ′ s.t. (I ′ , 〈M ′ ,N ′ 〉, 〈M,N〉)(ϕ) ̸= t.

Let (M1, N1) and (M2, N2) be MKNF interpretation pairs. We define an order of knowledge as: (M1,N1) ⪰k (M2,N2) iff M1 ⊆ M2 and N1 ⊇ N2. Then, a well-founded MKNF model of an MKNF formula ϕ is defined as a partial MKNF model (M,N) such that (M1,N1) ⪰k (M,N) for all threevalued MKNF models (M1, N1) of ϕ.

3 Well-Founded Semantics for HybridMKNF

A hybrid MKNF KB K = (O,P) consists of a decidable description logic (DL) knowledge base O, translatable into first-order logic, and a rule base P, a finite set of rules with modal atoms. The work of [Knorr et al., 2011] focuses on nondisjunctive rules (also see [Motik and Rosati, 2007]).

An MKNF rule r is of the form KH ← KA1, . . . , KAm, notB1, . . . , notBn, where Hi,Ai, and Bj are function-free first-order atoms. KH, {KAi}, and {notBi} are called the head (denoted Hd(r)), the positive body (Bd+(r)), and the negative body (Bd-(r)), respectively, and let Bd(r) = Bd+(r) ∪ Bd-(r). A rule is positive if it contains no notatoms and P is positive if all rules in it are positive.

Following [Motik and Rosati, 2010], we assume that MKNF rules are DL-safe; thus we can assume that rules are already grounded, if not said otherwise.

For the interpretation of a hybrid MKNF KB K = (O, P), a transformation π(K) = Kπ(O) ∧ π(P) is performed to transform O into a first-order formula and rules into a conjunction of first-order implications to make each of them coincide syntactically with an MKNF formula. Namely,

where ⃗x is the vector of free variables in r. In the sequel, we may just identify K with π(K) and P with π(P).

Definition 1. Let K = (O,P) be a hybridMKNFKB. KA(K) is the smallest set that contains all ground K-atoms occurring in P and modal atom Kφ if not φ occurs in P. A (partial) partition of KA(K) is a pair (T, P ), where T ⊆ P ⊆ KA(K). A partition of the form (T, T) is called exact.

We may overload the operator KA: given a set of modal atoms S, define KA(S) = {Kφ | Kφ ∈ S or not φ ∈ S}.

Intuitively, T contains true modal K-atoms and P contains possibly true modal K-atoms. Thus, the complement of P is the set of false modal K-atoms and P\T the set of undefined modal K-atoms.

The objective knowledge S ⊆ KA(K) is the set of firstorder formulas OBO,S = {π(O)} ∪ {ξ | Kξ ∈ S}.

There is a close relationship between partial partitions and MKNF interpretation pairs.

Definition 2. That a partition (T, P) of S ⊆ KA(K) is induced by an MKNF interpretation pair (M, N) is defined as: (i) Kξ ∈ T iff ∀I ∈ M, (I, 〈M,N〉, 〈M,N〉)(Kξ) = t; (ii) Kξ ̸∈ P iff ∀I ∈ M, (I, 〈M,N〉, 〈M,N〉)(Kξ) = f , and (iii) Kξ ∈ P\T iff ∀I ∈ M, (I, 〈M, N〉, 〈M, N〉)(Kξ) = u.

Let K = (O,P) be a positive hybrid MKNF knowledge base. We define the operator TK on subsets S of KA(K) :

As P is positive, TK is monotonic and thus it possesses a least fixpoint, which can be computed by the sequence 〈T iK〉∞i=0 , where T 0K = ∅, and T i+1 K = TK(T iK), for all i ≥ 0. Let us denote the least fixpoint of operator TK by lfp(TK).

Following [Knorr et al., 2011], we define two antitonic operators ΓK and Γ ′K for the computation of the least fixpoint of TK′ , where K′ is a positive hybrid MKNF KB obtained by two different transformations from K. Let S ⊆ KA(K). The MKNF transform of K relative to S, denoted K/S, is defined by K/S = (O, P/S), where P/S is obtained from P by (i) deleting each rule r in P such that KA(Bd-(r))∩S ̸= ∅, and (ii) deleting Bd-(r) from each remaining rule r.

To avoid potential conflicts between a DL knowledge base and rules, the MKNF-coherent transform, denoted K//S, is defined by K//S = (O, P//S), where P//S is the same as P/S, except that the condition (i) of the transform K/S is changed to: deleting each rule r such that KA(Bd-(r))∩S ̸= ∅ or OBO,S |=¬H, where Hd(r)=KH.

Since in both cases of K/S and K//S the resulting rule base is positive, a least fixpoint in each case exists. Let us define ΓK(S) = lfp(TK/S) and Γ ′K(S) = lfp(TK//S). Then, we can construct two sequences Pi and Ni, as follows:

The increasing sequence Pi is intended to compute modal K-atoms that are true, while the decreasing sequence Ni computes modal K-atoms that are possibly true, and at the end we reach a fixpoint pair (Pω, Nω), called alternating fixpoint pair of K, where Pω = ΓK(Nω) and Nω = Γ ′K(Pω).

Definition 3. Let K = (O,P) be a hybridMKNF knowledge base. If the alternating fixpoint pair (Pω,Nω) is a partition of KA(K), it is then called the well-founded partition of K.

4 Well-Founded Semantics Reclassified

Let us first cite the relevant theorems of [Knorr et al., 2011] that are under discussion here.

• Claim (1) (Theorem 1 in [Knorr et al., 2011]) If K is an MKNF-consistent hybrid MKNF KB, then a wellfounded MKNF model exists, and it is unique.
• Claim (2) (Theorem 2 in [Knorr et al., 2011]) Let K = (O,P) be a hybrid MKNF KB, Pω the fixpoint of Pi, and Nω the fixpoint of Ni. K is MKNF-inconsistent iff Γ ′K(Pω) ⊂ ΓK(Pω) or Γ ′K(Nω) ⊂ ΓK(Nω), or O is inconsistent.
• Claim (3) (Theorem 4 in [Knorr et al., 2011]) Let K = (O, P) be an MKNF-consistent hybrid MKNF KB and (Pω,Nω) the well-founded partition of K. Then (IP , IN) is a three-valued MKNF model of K, where (IP , IN) = ({I | I |= OBO,Pω }, {I | I |= OBO,Nω }).

Below, we show two counterexamples to these claims.

Example 1. Let K = (O,P), where O = ¬c and P = {Ka ← not b; Kb ← not a; Kc ← Ka}. It can be verified that (M,M), where M = {{b}, {b, a}}, is a total three-valued MKNF model of K, and thus K is MKNFconsistent. One can verify that the alternating fixpoint pair of K, which is also the well-founded partition of K, is (Pω, Nω) = (∅, {Ka, Kb}). From Γ ′K(Pω) = {Ka, Kb} and ΓK(Pω) = {Ka, Kb, Kc}, we get Γ ′K(Pω) ⊂ ΓK(Pω). Then by Claim (2) above, K is MKNF-inconsistent.

From (Pω, Nω) we get an MKNF interpretation pair

which is not a three-valued MKNF-model of K, since for any I, the three-valued MKNF structure (I, 〈IP , IN〉, 〈IP , IN〉) evaluates [Kc, K¬c, Ka, Kb, not a, not b] to [f , t, u, u, u, u], in which the last rule in P is not satisfied. Therefore, Claim (3) is erroneous too.

For this example Claim (1) holds, as (M,M) is the only three-valued MKNF model of K and it is thus least defined and the well-founded MKNF model of K.

Example 2. Let us consider K = (O, P), where O = (a ⊃ h) ∧ (b ⊃ ¬h) and P = {Ka ← not b; Kb ← not a}. Consider two partitions, ({Ka}, {Ka}) and ({Kb}, {Kb}). The corresponding MKNF interpretation pairs turn out to be twovalued MKNF models of K. Hence, K is MKNF-consistent.

The well-founded partition of K is (Pω,Nω) = (∅, {Ka,Kb}). Applying the conditions in Claim (2), since Γ ′K(Nω) = ΓK(Nω) = ∅, Γ ′K(Pω) = ΓK(Pω) = {Ka, Kb}, and O is consistent, no inconsistency is detected. That is, for this example Claim (2) holds. But here, there is no three-valued MKNF interpretation pair (M,N) for the wellfounded partition (∅, {Ka,Kb}), as OBO,{Ka,Kb} is unsatisfiable and thus N = ∅, while by definition a three-valued MKNF interpretation pair must satisfy the condition ∅ ⊂ N ⊆M. As a result, for this example Claim (3) fails.

Since the above two-valued MKNF models are not comparable w.r.t. undefinedness and we can show that no other three-valued MKNF models exist, Claim (1) fails too.

In general, we want our well-founded model to be minimal, unique, and computable by an iterated construction, the three properties that are typically associated with any notion of a well-founded model in logic programming. The notion of a well-founded MKNF model by Knorr et al. satisfies the first two but not the third, while the alternating fixpoint construction is not guaranteed to generate a partition that corresponds to a three-valued MKNF model, even when such a model exists. This suggests that we can pursue the correct relationships between the concepts introduced in [Knorr et al., 2011], which leads to a classification of hybrid MKNF knowledge bases by a hierarchy of three classes, in addition to the class of all hybrid MKNF knowledge bases.

Definition 4. Let K = (O,P) be a hybrid MKNF KB and (Pω,Nω) its alternating fixpoint pair.

• K is MKNF-consistent if K has a three-valued MKNF model (the definition is unchanged).
• K is MKNF-strongly consistent if K has a well-founded MKNF model.
• K is MKNF-coherent if ({I | I |= OBO,Pω }, {I | I |= OBO,Nω }) is a three-valued MKNF model of K.

It can be shown that each class is a strict subset of the one above it and the class of MKNF-coherent MKNF KBs is the one intended by the well-founded semantics of Knorr et al.

5 Characterizations

We generalize the rule evaluation scheme of [Motik and Rosati, 2010] from the two-valued case to the three-valued one, with the goal of relating the rule evaluation by a (partial) partition with the rule evaluation by a three-valued MKNF structure. Let K = (O, P), let T and F be subsets of KA(K) such that T ∩ F = ∅, and let r be a rule in P. The rule r[K, T, F] is obtained by replacing each modal atom Kξ in r with t if Kξ ∈ T, with f if Kξ ∈ F, and with u otherwise. Similarly, the rule r[not , T, F] is obtained by replacing each modal atom not ξ appearing in r with t if Kξ ∈ F, with f if Kξ ∈ T, and with u otherwise. Finally, r[T, F ] = r[not , T, F ][K, T, F ].

In all these cases, the result is simplified as follows:

• If the value of the head atom in a rule is equal to or greater than the value of its body, then the rule is replaced by t ←.
• If the value of the head atom in a rule is less than the value of its body, then the rule is replaced by f ←.

The rule sets P[K, T, F], P[not , T, F], and P[T, F] are obtained by replacing each rule r in P, respectively, with r[K, T, F ], r[not , T, F ], and r[T, F ]. We write P[K, T, F ] = t if each rule in P is of the form t ←, or P = ∅; similarly, we write P[K, T, F ] = f if P contains a rule of the form f ←.

We now define the important notion called stable partition.

Definition 5. Let K = (O,P) be a hybrid MKNF KB and T ⊆ P ⊆ KA(K). (T, P) is a stable partition of K if

1. OBO,P is satisfiable;
2. (i) ∀Kξ ∈ KA(K), if OBO,T |= ξ then Kξ ∈ T and if OBO,P |= ξ then Kξ ∈ P; and (ii) in addition, P[T, KA(K) \ P ] = t; and
3. for any other partition (T ′ , P ′ ) with T ′ ⊆ T and P ′ ⊆ P, where at least one of the inclusions is proper,
4. (i) ∃Kξ ∈ KA(K) \ T ′ , OBO,T ′ |= ξ, or ∃Kξ ∈ KA(K) \ P ′ , OBO,P ′ |= ξ, or
5. (ii) P[not , T, KA(K) \ P ][K, T ′ , KA(K) \ P ′ ] = f

The notion of a stable partition imitates that of three-valued MKNF models by performing specific checks. Condition (1) requires that the DL component O be consistent with P, which guarantees the consistency of O with T (due to T ⊆ P). Condition (2) makes sure that (T, P) "satisfy" Kπ(O) as well as rules in P; in both cases we are able to devise simple checks to achieve the goal. In (3), we minimize the derivation of modal K-atoms by not allowing any smaller T ′ and reduce the undefined by not permitting any smaller P ′ , so that (T ′ , P ′ ) can still "satisfy" Kπ(O) on the one hand and π(P) on the other.

Theorem 1. Let K = (O,P) be a hybrid MKNF KB..

• (I) If an (MKNF) interpretation pair (M,N) is a threevalued MKNF model of K, then the partition (T, P) induced by (M, N) is a stable partition of K.
• (II) If a partition (T, P) is a stable partition of K, then the interpretation pair (M,N), where (M,N) = ({I | I |= OBO,T}, {I | I |= OBO,P}), is a three-valued MKNF model of K.

Given two partitions (T, P ) and (T ′ , P ′ ), we define an order of precision ⊆p as: (T, P) ⊆p (T ′ , P ′ ) if T ⊆ T ′ and P ′ ⊆ P. As (T, P) and (T ′ , P ′ ) are partitions, they satisfy T ⊆ P and T ′ ⊆ P ′ ; therefore (T, P) ⊆p (T ′ , P ′ ) expresses T ⊆ T ′ ⊆ P ′ ⊆ P. Intuitively, the pair (T ′ , P ′ ) is more precise (in fact, no less precise) than (T, P) in terms of truth and falsity of modal atoms, and is an approximation to the full precisions, which are exact partitions (Q, Q) such that Q is in between T ′ and P ′ . This is the familiar notion of approximation given in [Denecker et al., 2004].

The order of precision ⊆p defined here for partitions is the counterpart of the order of knowledge ⪯k defined for MKNF interpretation pairs. We thus can define a hierarchy for hybrid MKNF knowledge bases, similar to that of Def. 4, but this time based on the properties of the precision order, and establish the relevant relationships among its subclasses.

A major advantage of representing three-valued MKNF models in terms of stable partitions is that it allows us to compute three-valued MKNF models using a relatively straightforward guess-and-check approach - guess a partition (T, P) and check whether (T, P) is stable.

Theorem 2. Let K = (O,P) be a hybrid MKNF KB and (T, P) a partition of K. Then, (T, P) is a stable partition iff T = ΓK(P), P = Γ ′K(T), and OBO,ΓK(T) is satisfiable.

The relationship given above sheds light on how to devise a DPLL style solver for semantics based on two-valued/threevalued MKNF models. It also leads to the following results.

Proposition 1. Let K be a nonground but DL-safe hybrid MKNF KB, and assume that the entailment of ground literals in the language of O is decidable with data complexity C. Then, the data complexity of deciding whether a threevalued MKNF model exists, or deciding whether a two-valued MKNF model exists, is in NPPTimeC . If C is tractable, the same decision problem for both is NP-complete.

These results are consistent with those of [Knorr et al., 2011; Motik and Rosati, 2010], except that the NPcompleteness result for deciding the existence of a threevalued MKNF model is new.

Acknowledgments

This work is partially supported by Shanghai Innovation Action Plan Project under the grant No. 16511101200 and NSERC discovery grant RGPIN 05642.