Combining answer set programming with ontologies is of great theoretical and practical interest. Hybrid MKNF is a semantics that combines ASP with ontologies without increasing the solving complexity. While there are eficient solvers for ASP and ontologies, eficient solvers for hybrid MKNF have yet to be constructed. In this work, we address some issues that must be solved before a CDNL-based (conflictdriven nogood learning) solver for hybrid MKNF knowledge bases can be developed. We formulate a framework to characterize disjunctive hybrid MKNF semantics through a family of fixpoint operators, then contextualize this framework by demonstrating that it could be possible to integrate it into a solver. Crucially, our approach can be performed without relying on a dependency graph. Finally, we recognize a property of our characterization that is analogous to head-cycle free disjunctive logic programs and demonstrate how to exploit this property to improve solver eficiency.
logic and ASP without increasing complexity [
In this work, we present a framework for disjunctive hybrid MKNF knowledge bases that utilizes fixpoint operators. This framework does not rely on dependency graphs and the only restriction it imposes on the description logic is that the entailment relation can be checked in polynomial time.
Numerous accounts on the complexity of disjunctive ASP [
Minimal knowledge and negation as failure (MKNF)[
An MKNF interpretation is a set of first-order interpretations (“possible worlds”) and we
say that satisfies a formula , written |= , if (, , ) |= for each ∈ .
An MKNF model of a formula is an MKNF interpretation such that |= and
there does not exist an MKNF interpretation ′ ⊃ such that (, ′, ) |= for each
∈ ′. Following Motik and Rosati [
K 1, . . . , K ←
K +1, . . . , K , not +1, . . . , not (1) In the above, 1, . . . , are function-free first-order atoms. Given a rule ∈ , we define the following abbreviations:
Let () denote rule set ’s corresponding MKNF formula:
head() = {K 1, . . . , K }, +() = {K +1, . . . , K }, − () = {not +1, . . . , not }, K (− ()) = {K | not ∈ − ()}, and
body() = (+(), K (− ())) () = ⋀︁ (), where ∈ () = ⋁︁ K ⊂ =1 ⋀︁ =+1 ⋀︁ =+1 K ∧ not
The semantics of a hybrid MKNF knowledge base is obtained by applying both transformations to and and placing within a K operator, i.e. () = () ∧ K (). We use , , and in place of (), (), and () respectively when it is clear from context that the respective translated variant is intended. We refer to formulas of the form K and not as K-atoms and Not-atoms respectively. When it is clear from context, we may write a bare atom in place of a K-atom K . Throughout this work, we assume that MKNF formulas are ground, i.e., they contain no variables.
We now outline some definitions and conventions. For a hybrid MKNF knowledge base = (, ), we denote the set of all modal atoms found within as KA() where KA() is defined as follows.
KA() = {K | either K or not occurs in the head or body of a rule in } The objective knowledge of a hybrid MKNF knowledge base w.r.t. a set of K-atoms ⊆ KA() is the set of first-order formulas { ()} ∪ { | K ∈ }. We denote this set as OB,S .
A (partial) partition of KA() is a disjoint pair of subsets of KA(). We usually denote a partition as (, ). K-atoms in are said to be true and K-atoms in are said to be false. A partition is total if ∪ = KA(). We frequently treat (, ) as an interpretation that contains only K-atoms. A dependable partition is a partial partition (, ) with the additional restriction that OB,T ∪ {¬} is consistent for each K ∈ or OB,T is consistent if is empty. A partial partition that is not dependable may not be extended to an MKNF model. A rule body is applicable w.r.t. a partition (, ) if body() ⊑ (, ), i.e., if +() ⊆ and K (− ()) ⊆ . We say that an MKNF interpretation of induces a partition (, ) if ⋀︁ |= K ∧ K ∈
⋀︁ |= ¬K K ∈ (2) Note that the partition ( * , * ) induced by an MKNF model is unique and dependable. For a partition (, ) that is a subset of this ( * , * ), i.e., (, ) ⊑ ( * , * ), we say that (, ) can be extended to an MKNF model; such a partition is also dependable.
In this section, we formulate a framework that relies on fixpoint operators to represent MKNF models. First consider the MKNF knowledge base = (, ) where () = {(∨) ⊃ } and only contains the rule K , K ← not . This knowledge base has no MKNF models. Intuitively, we can verify that does not have an MKNF model by recognizing that there is no rule to derive K and thus some K-atom in the head of this rule must be true in an MKNF model of . With either K or K true, an inconsistency is created if K is false.
We generalize and formally express these intuitive semantics by considering head-cuts of . We define a head-cut of to be a set ⊆ × KA() where each rule ∈ occurs in no more than one pair (, ℎ) ∈ and K ℎ ∈ head(). For example, the program = {K , K ←} , has exactly two head-cuts, {(, )} and {(, )} where refers to the only rule in (Note that we omit “K ” when describing head-cuts). Given a head-cut , we use head() and rule() to denote the sets {ℎ | (, ℎ) ∈ } and { | (, ℎ) ∈ } respectively.
Definition 4.1. For a total partition (, ), we define (, ) to be the set containing every head-cut of such that head() ⊆ and for each rule ∈ , ∈ rule() if and only if body() ⊑ (, ).
Intuitively, there is a head-cut in (, ) for each way of selecting a single head-atom for every satisfied rule in . In essence, (, ), gives us a way to avoid dealing with negation or disjunction. We use this set to show atoms are justified by defining a family of operators induced by a head-cut : () ={K ℎ | where (, ℎ) ∈ and +() ⊆ for each ∈ }
∪{K ∈ KA() | OB,X |= } We denote the least fixpoint of an operator as lfp and use to denote applying the operator times on the empty set (e.g., 2 = ((∅))). This operator simply takes a set of K-atoms and extends it with immediate consequences under .
Revisiting the initial example where = (, ), () = {( ∨ ) ⊃ }, and = {K , K ← not }, consider any total dependable partition (, ) where K ∈ . Observe that for each head-cut ∈ (, ), we have ∈ lfp . For example, let (, ) = ({K }, {K , K }). Every head-cut in (, ) contains the rule from , thus the op erator will compute either or on the first iteration and then on the second iteration. Conversely, if we consider a dependable partition (, ) such that K ∈ , then for each head-cut ∈ (, ), we have ̸∈ lfp . For example, let (, ) = ({K , K }, {K }).
No rule in is applicable w.r.t. (, ), thus (, ) contains a single head-cut, ∅. We have ∅0 = ∅1 = ∅, thus ̸∈ lfp .
We now formally show that sets of the form (, ) coincide with an MKNF models of hybrid knowledge bases. First, we connect family of sets (, ) to total partitions that satisfy all rules in but are not necessarily induced by an MKNF model.
Lemma 4.1. For a total partition (, ), the set (, ) is empty if and only if there exists a rule ∈ where body() ⊑ (, ) and head() ∩ = ∅.
Definition 4.2. A set of head-cuts is a supporting set for a total dependable partition (, ) if: An MKNF model of that induces (, ) exists if and only if is nonempty and for each ∈ the set computed by lfp is precisely .
Proposition 4.1. The set (, ) is a supporting set of the dependable partition (, ).
In the following example, we demonstrate how the set (, ) can be used to verify that a partition can be extended to a model. Example 1. Let = (∅, ) where is defined as 1 : K , K ←
K 2 : K , K ← Let (, ) = ({K , K }, {K }). By definition, the set (, ) contains two head-cuts: 0 = {(1, ), (2, )} and 1 = {(1, ), (2, )}. When we repeatedly apply the operator on each of these head-cuts we obtain the following sets.
00 = ∅ 01 = ∅ 10 = {} 11 = {} 20 = 10 21 = {, } 30 = 10 31 = 21
Using Proposition 4.1, it is easy to confirm that (, ) = ({K , K , K }, ∅) can not be extended to a model of by observing that neither lfp 0 nor 1 computes . If we instead use (, ) = ({K , K }, {K }), then the set (, ) contains the just a single head-cut, 0 = {(1, ), (2, )}.
We have lfp 0 = , thus (, ) can be extended to an MKNF model.
Now that we have established a semantics in terms of a family of fixpoint operators, we discuss some optimizations that, when applied to (, ), greatly reduce the number of head cuts in the set. This is a crucial step that enables the set to be used in a solver. For a dependable partition (, ), that cannot be extended to a model, there are many head-cuts in (, ) that contain rules whose bodies are never satisfied by iterative construction or do not derive anything new. Our first optimization step is to remove such rules from head-cuts by defining a new set (, ) based on (, ). A head-cut is in (, ) if and only if there is a head-cut ′ ∈ (, ) such that = ′ ∖ , where
= {(, ℎ) ∈ | ∀, body() ⊆ =⇒ head() ⊆ } This set removes some pairs in each head-cut from (, ). For each head-cut ∈ (, ) there is some head-cut ′ ∈ (, ) for which ⊆ ′. However, ′ is not unique in general.
The set (, ) also has the convenient property of only including pairs that contribute to the computation of , thus head() ⊆ lfp .
In the example following example, we demonstrate that (, ) can be used as a supporting set. Example 2. Let = (∅, ) where contains the following rules Let (, ) = (KA(), ∅) and = {(0, ), (1, ), (3, )}. 1 computes “” via rule 0, then 2 computes “” via rule 2. On the third iteration, 3 computes “” via rule 3, however, we already have head(3) ⊆ 2, thus is not in (, ). Instead, the head-cut = {(0, ), (1, )} is in (, ).
Like (, ), the set (, ) is a supporting set of (, ).
Proposition 4.2. (, ) is a supporting set of (, ).
We define more optimizations that further reduce the number of head-cuts that need to be tested to verify a model. A head-cut is branch-minimal w.r.t. a set of head-cuts if for each ′ ∈ such that head() ⊆ head(′) or head(′) ⊆ head(), we have head() ⊆ head(′). It can be easily shown that this relation is a partial order between head-cuts.
We formulate a further optimization of (, ) based on this notion of minimality.
(, ) = { ∈ (, ) | is branch-minimal w.r.t. (, )} Proposition 4.3. (, ) is a supporting set of (, ).
The set (, ) is not practical for use in solver: Because of the complexity of determining whether a head-cut is branch-minimal, the set cannot be eficiently enumerated. We develop a supGpiovretninag hseetadth-cauttisa, cwomepdreofinmeiseo[f]tob(e,th)e. subset of that contains only the rules in rule() whose bodies are satisfied after iterations of the operator, that is,
[] = {(, ℎ) ∈ | ℎ ̸∈ , +() ⊆ } Intuitively, [] contains the atoms newly derived on iteration . Likewise, we define a range [0..] where 0 ≤
A head-cut is semi-branch-minimal w.r.t. a head-cut ′ if for the largest such that [0..] = ⋃︁ []
=0 [0..( − 1)] = ′[0..( − 1)] we have head([]) ⊆ head(′[]).
We define (, ) to be the set
(, ) = { ∈ (, ) | is semi-branch-minimal w.r.t. every other head-cut ′ ∈ (, )} We give an example of a head-cut from (, ) that is also in (, )
Example 3. Let = (, ) where = ∅ and Let (, ) = (KA(), ∅). Define the following head-cuts: 1 :K , K ← 2 :K , K ← 3 :K ←
K
K
0 = {(1, ), (2, ), (3, )},
1 = {(1, ), (2, ), (3, )},
2 = {(1, ), (2, ), (3, )},
3 = {(1, ), (2, ), (3, )}
We have (, ) = {0, 1, 2, 3}. For each pair of head-cuts and , we have [0..1] =
[0..1]. However, we have head(0[
Example 4. Let = (, ) such that = ∅ and = {1 : K , K , K , K ← ; 2 : K , K , K ← ;
K ← ; K ← ; K ← ; K ← ; K ← ; K ← ; } We use the total partition (, ) = (KA(), ∅) to consider various head-cuts in the sets (, ) ahneadd-cut(,fo).uFnodribnrevity(,w,e) obmutitnpoatirs in(h,ea)d.-cuts that contain normal rules. First, we give a
= {(1, ), (2, )} 1 = {} lfp = {, , , }
= {(1, ), (2, )} 1 = {, } lfp = {, , } not (, ):
is semi-branch-minimal w.r.t. every head-cut from (, ) because head() contains a single atom and there is no head-cut ′ in (, ) such that head(′) = ∅. However, the selection of in results in the atoms , , and , also being derived; For the head ′ = {(1, ), (2, )}, lfp ′ = {, , }, thus is not branch-minimal. We give a head-cut that is in (, ) and is branch-minimal because every head-cut in (, ) computes at least , , and , however, is not semi-branch-minimal because ∈ head(); A head-cut in (, ) cannot contain a pair with in it because there is always a head-cut ′ that is semi-branch-minimal w.r.t. .
We give an exhaustive account of the head-cuts that are in both (, ) and (, ): 0 = {(1, ), (2, )} 1 = {(1, ), (2, )} lfp 0 = lfp 1 = {, } As mentioned above, no head-cut in (, ) can have ∈ head() and no head-cut in (, ) can have ∈ head(), thus no head-cut in (, ) ∩ (, ) can contain either (, ):
atom. Finally, we give an example of a head-cut in (, ) that is neither in (, ) nor = {(1, ), (2, )} 1 = {, } lfp = {, , , } The head-cut demonstrated above is neither branch-minimal nor semi-branch-minimal.
(, ) and (, ) are disjoint, they are related in a crucial way that allows
Even though (, ) is a supporting set. Intuitively, a head-cut from us to show that (, ) can be thought of as having a minimal set head() that is globally minimal w.r.t. iterations of whereas a head-cut from (, )’s set head() is only locally minimal w.r.t. an iteration of . As it turns out, (, ) that fails to (, ) is more precise and if there is a head-cut in compute , we can guarantee that such a head-cut exists in (, ) as well. We demonstrate this property formally. (, ) such that lfp ⊂ , then there is a Lemma 4.2. If there exists a head-cut in ∈ head-cut ′ ∈ (, ) ∩ (, ) such that lfp ′ ⊂
Finally, we can use the property demonstrated above to show that (, ) is a supporting set of (, ).
Proposition 4.4. (, ) is a supporting set of (, ).
Up until now, we have dealt exclusively with total partitions. We now discuss how the techniques described in the previous section can be applied to partial partitions and in turn be used to develop an abstract solver.
We define the set under a head-cut .
= {( * , * ) | where = * [0..] for some and * ∈ ( * , * ) and total partition ( * , * )}
Given a head-cut , we can extract an appropriate partition from :
() = (lfp , ⋃︁{− () | (, ℎ) ∈ }) Note that for each ( * , * ) ∈ , we have () ⊑ ( * , * ). Intuitively, the set holds every possible set ( * , * ) if () were extended to a total partition ( * , * ). Note that ( * , * ) may not be dependable. We also define a total variant of ():
* () = (lfp , KA() ∖ lfp ) We recursively define a subclass of head-cuts to limit the use of . Definition 5.1. Given, a head-cut where () is a dependable partition, we call a headcut state if either = ∅ or there is another head-cut state ′ such that either = ′[0..] or ∈ ⋃︀ ′ .
Intuitively, a head-cut state is a head-cut that can be extended to some a head-cut in ∈ for every ∈ . Note that () ⊑ * () for a head-cut state .
We now define an abstract solver that operates on head-cut states. Supporting can assist a solver in several key ways: Conflict propagation and immediate propagation that adds positive direct consequences to a head-cut state (See () in Algorithm 1), Guiding solver decisions at points where the current head-cut state cannot be extended through means of well-founded propagation (See () in Algorithm 2) and as already shown, supporting sets can be used for model verification. We join these roles together in an abstract solver outlined in Algorithm 3. Finally, we show how supporting sets can be used to reason about head-cut states that can be verified in polynomial time (similar to head-cycle free). We leave certain details unspecified such as how to enumerate the set in an eficient way in the context of each of the algorithms and the overall complexity of the algorithms we provide.
Algorithm 1: () 1 (, ) ← (); 2 ← { ′[ + 1] | ′ ∈ ⋃︀ , ′[0..] = }; 3 if ∃(, ℎ) ∈ ⋂︀ , |head() ∖ | ̸= 1 or body() ̸⊑ (, ) then 4 return ; 5 assert || ≤ 1; 6 return ∪ ⋂︀ ;
Intuitively, Algorithm 1 adds information to only if there are only rules whose bodies are satisfied w.r.t. () and the head of the rule contains no true atoms and only a single atom that is not false. We demonstrate that a solver cannot miss any models by applying () to a head-cut state.
Lemma 5.1. For a head-cut state and any head-cut * ∈ ⋃︀ where = * [0..], we either have * [0..( + 1)] = () or = ().
With (), we only propagate information if it holds in all models that () can be extended to. At some point in the solving process, we must add information for which this does not hold. We describe a process for extending head-cut states with decision atoms.
Algorithm 2: () 1 ← ∅ ; 2 if ∈ ⋃︀ then 3 return ∅; 4 for ′ ∈ ⋃︀ where ∃, ′[0..] = do 5 if (′[0..( + 1)]) is dependable then 6 ← ∪ {′[0..( + 1)]}; 7 return ;
We guarantee very little about the atoms added by () and in general, the solver will be forced to backtrack because of the atoms that were added by this procedure. However, extensions made by () will maintain the property that is a head-cut state. Furthermore, if () can be extended to an MKNF model of , then a head-cut in () also has this property. This ensures that a solver that uses () will not miss any models. Lemma 5.2. Given a head-cut state and an MKNF model that induces (), there is either a head-cut state ′ ∈ () such that induces (′) or () is empty.
We define check-model() to be a procedure that simply enumerates all head-cuts in * () to verify that * () can be extended to a model by applying the until a fixed point is reached. The correctness of such an algorithm follows directly from Proposition 4.4.
We now integrate all preceding algorithms into an abstract solver.
Algorithm 3: () 1 ← lfp (); 2 for ′ ∈ () do 3 if (′) then 4 return (′); 5 if () = ∅ and check-model() then 6 return * () 7 return ;
While we do not specify which head-cut from () should be selected to minimize backtracking, our algorithm can locate a model if one exists.
Lemma 5.3. Given a head-cut state , if there exists a model that induces (), then () will return a total partition induced by a model.
While more eficient than a guess-and-verify solver, Algorithm 3 does not eficiently verify total partitions. It is well known that head-cycle free disjunctive logic programs can be solved in NP [12]. We demonstrate an analogous subclass of disjunctive MKNF knowledge bases that can be verified in polynomial time.
First, we identify a property of head-cut states that enables polynomial verification. We show that this property holds if and only if a head-cut state coincides with an MKNF model. Definition 5.2. A head-cut state is P-verifiable if the following holds. For every head-cut * ∈ ⋃︀ , where * [0..] = [0..] and * [ + 1] ̸= [ + 1], we have lfp * ⊇ head([ + 1]). Proposition 5.1. If a head-cut state is P-verifiable and * () is dependable, then lfp = if and only if lfp ′ = for each ′ ∈ * ().
Corollary 5.1. A head-cut state is P-verifiable if and only if * () can be extended to an MKNF model of .
Using the above property, we construct a verification algorithm that is more eficient than check-model().
Algorithm 4: check-model2() 1 if * () = ∅ then
2 return ; 4 for 0′; ∉ =*(−1);w h←ere +[01..do]= ′[0..] and [ + 1] ̸= ′[ + 1] do 3 for ← 5 if head([ + 1]) ̸⊆ lfp ′ then 6 return ; 7 return ;
When check-model() is replaced with Algorithm 4 in the solver (Algorithm 3), P-verifiable head-cut states can be quickly verified. We feel strongly that with further complexity analysis we will be able conclude that our abstract solver algorithm, when used with an empty ontology and head-cycle free disjunctive logic program, can verify any enumerated partition in polynomial time.
We have provided a new way of characterizing disjunctive MKNF models through supporting sets. The largest set we defined, (, ), contains many redundant head-cuts and is not practical for use in a solver. We defined a sm aller set, (, ), where each head-cut in (, ) is limited to rules that contribute to the fixpoint computation. Next we refined (, ) further to obtain (, ) and the less precise but more tractable set (, ). We provided an abstract solver that utilizes supporting sets to enumerate partitions and to verify models. Finally, we characterized P-verifiable head-cut states, a property of head-cut states that is comparable to head-cycle-free disjunctive logic programs, and we give a more eficient model verification procedure that leverages this property.
We speculate that the complexity of our abstract solver algorithm is no worse than a guessand-verify solver if the entailment relation of the accompanying ontology can be computed in polynomial time. We also speculate that if the ontology is empty and is a head-cycle free disjunctive logic program that the complexity of finding a model lies in . However, we leave a full analysis of the complexity of our algorithm and the complexity of recognizing P-verifiable head-cut states to future work. In this work, we introduce many new structures to characterize our semantics; It would be interesting to recast this work using more familiar ifxpoint structures such as approximators in approximation fixpoint theory [ 13]. In the future, we would also like to leverage this framework to generate conflicts so that a CDNL-based solver may be constructed. [12] R. Ben-Eliyahu, R. Dechter, Propositional semantics for disjunctive logic programs, Ann.
Math. Artif. Intell. 12 (1994) 53–87. [13] F. Liu, J. You, Alternating fixpoint operator for hybrid MKNF knowledge bases as an approximator of AFT, in: P. Fodor, M. Montali, D. Calvanese, D. Roman (Eds.), Rules and Reasoning - Third International Joint Conference, RuleML+RR 2019, Bolzano, Italy, September 16-19, 2019, Proceedings, volume 11784 of Lecture Notes in Computer Science, Springer, 2019, pp. 113–127.