The logic of hybrid MKNF (Minimal Knowledge and Negation as Failure) enables tight interwoven reasoning between answer set programming and open-world reasoning systems. The presence of both classical negation and negation as failure poses significant semantic challenges on issues that must be addressed before practical systems can be built. In this work, we improve well-founded reasoning for hybrid MKNF knowledge bases. Unlike traditional answer set programming, the well-founded semantics for hybrid MKNF is intractable. Prior work established a class of knowledge bases with known polynomial-time algorithms to compute their well-founded models and in this paper, we improve upon this work by expanding this class. We provide a new fixpoint operator for computing well-founded models and compare our operator to prior work.
In this work, we present a well-founded operator that can compute the well-founded models for a larger class of knowledge bases than the previous state-of-the-art operators. Prior work on well-founded semantics has diverged in method with non-overlapping advancements and our work unifies these advancements and extends them further. We provide an in-depth analysis of prior operators to compare semantic diferences and ultimately show that our new operator subsumes prior work.
Namely, prior operators are limited in the inferences they can make that rely on classically false information. The mixing of negation as failure and classical falsity is strong reason to use hybrid MKNF, however, current fixpoint operators do not make full use of classically false information. Our advancements are general-purpose and can improve inference power on a wide variety of problem domains.
Because a given knowledge base may not have a well-founded model, well-founded operators are sound but not necessarily complete. The fixpoint of a sound operator will always be less precise or as precise as the well-founded model if a well-founded model exists.
Section 2 details necessary preliminaries and establish notation used throughout this work.
Section 3 discusses the well-founded semantics of hybrid MKNF knowledge bases. In Section 4,
we present a fixpoint characterization of hybrid MKNF knowledge bases that expands the class
of knowledge bases with polynomial well-founded semantics. In Section 5, we give a granular
breakdown of the diferences between our operators and prior operators. Finally, we summarize
and conclude in Section 6.
2. Preliminaries: Hybrid MKNF Knowledge Bases
MKNF (Minimal Knowledge and Negation as Failure) is a nonmonotonic logic formulated by
Lifschitz [
While there are many hybrid frameworks that combine ASP with an external system, Motik
and Rosati list several key properties of hybrid MKNF knowledge bases that make it suitable for
embedding description logics [
Partial model semantics have numerous advantages over their two-valued counterparts. They
can serve as the basis for grounding algorithms as well as increase the scalability of a reasoning
system by leaving some truth values unspecified. We adopt Knorr et al.’s [
1 and ⊇ an MKNF structure is defined as follows: with the term .
Hybrid MKNF relies on the standard name assumption under which every first-order interpretation in an MKNF interpretation is required to be a Herbrand interpretation with a countably infinite amount of additional constants. We use ∆ to denote the set of all these constants. We use [ → ] to denote the formula obtained by replacing all free occurrences of variable x in
A (3-valued) MKNF structure is a triple (, ℳ, ) where is a (two-valued first-order) interpretation and ℳ = ⟨, 1⟩ and = ⟨, 1⟩ are pairs of sets of first-order interpretations 1. Using and to denote MKNF formulas, the evaluation of (, ℳ, )((1, . . . , )) := (, ℳ, )(¬) := ⎧ t ⎨ ⎩ f
if (, ℳ, )() = f u if (, ℳ, )() = u if (, ℳ, )() = t ︂{ t if (1, . . . , ) is true in f if (1, . . . , ) is false in (, ℳ, )(∃, ) := {(, ℳ, )([ → ]) | ∈ ∆ } (, ℳ, )(∀, ) := {(, ℳ, )([ → ]) | ∈ ∆ } (, ℳ, )( ∧ ) := ((, ℳ, )(), (, ℳ, )( )) (, ℳ, )( ∨ ) := ((, ℳ, )(), (, ℳ, )( )) (, ℳ, )( ⊂ ) := (, ℳ, )(K) := (, ℳ, )(not ) := {︃ t if (, ℳ, )() ≥ (, ℳ, )( ) f
otherwise ⎧ t ⎨
f ⎩ u ⎧ t ⎨
f ⎩ u otherwise if (, ⟨, 1⟩, )() = t for all ∈ if (, ⟨, 1⟩, )() = f for some ∈ 1 otherwise if (, ℳ, ⟨, 1⟩)() = f for some ∈ 1 if (, ℳ, ⟨, 1⟩)() = t for all ∈ Intuitively, ℳ and are collections of possible worlds (two-valued first-order interpretations). The modal K and not operators check whether a condition holds for every possible world in ℳ and respectively. ℳ and are pairs of sets of possible worlds so that we can encode the third truth value, u. It is this separation of the evaluation of K and not that allows us to avoid transforming a program into its “reduct” as is done in stable model semantics.
The logic of MKNF as described above is very general, but we restrict our focus to hybrid MKNF Knowledge bases, a syntactic restriction that captures combining answer set programs with ontologies. An (MKNF) program is a set of (MKNF) rules. A rule is written as follows: Kℎ ←
K0, . . . , K , not 0, . . . , not .
In the above, the atoms ℎ, 0, 0, . . . , , and are function-free first-order atoms of the form (0, . . . , ) where is a predicate and 0, . . . , are either constants or variables. We call an MKNF formula ground if it does not contain variables. The corresponding MKNF formula () for a rule is as follows: () := ∀⃗, Kℎ ⊂ K0 ∧ · · · ∧
K ∧ not 0 ∧ · · · ∧ not where ⃗ is a vector of all variables appearing in the rule. We will use the following abbreviations: () := ⋀︁ () ℎ() = Kℎ
∈ +() = {K0, . . . , K } − () = {not 0, . . . , not }
K(− ()) = {K | not ∈ − ()} interpretation pair ( ′, ′) where ⊆ ∈ ′ s.t. (, ⟨ ′, ′⟩, ⟨, ⟩)( ()) ̸= t.
This ensures that is decidable. reasoning with the ontology can be performed in polynomial time.
An ontology is a decidable description logic (DL) knowledge base translatable to first-order logic, we denote its translation to first-order logic with (). We also assume that entailment
A normal hybrid MKNF knowledge base (or knowledge base for short) = (, ) contains
a program and an ontology. The semantics of a knowledge base corresponds to the MKNF
formula () = () ∧ K (). We assume, without loss of generality [
A (3-valued) MKNF interpretation (, ) is a pair of sets of first-order interpretations where ∅ ⊂ ⊆
. We say an MKNF interpretation (, ) satisfies a knowledge base = (, )
A (3-valued) MKNF interpretation (, ) is a (3-valued) MKNF model of a normal hybrid MKNF knowledge base if (, ) satisfies () and for every 3-valued MKNF ′, ⊆ ′, (, ) ̸= ( ′, ′), and we have some
Intuitively, minimal knowledge is captured by adding more possible worlds to the MKNF interpretation used to evaluate K-atoms (the evaluation of not -atoms stays the same). The more possible worlds there are, the more likely it is for K to be false. objective knowledge w.r.t. to a set of K-atoms .
It is often convenient to only deal with atoms that appear inside . We use KA() to denote the set of K-atoms that appear as either K or not in the program and we use OB, to the ︁( KA() := {K | ∈ , K ∈ {ℎ()} ∪ +() ∪ K(− ()) } ︁) OB, := {︀ ()}︀
∪ ︀{ | K ∈ }
1Not every knowledge base can be grounded. The prevalent class of groundable knowledge bases is the knowledge
bases that are DL-safe [
A K-interpretation ( , ) ∈ ℘(KA())2 is a pair of sets of K-atoms2. We say that ( , ) is consistent if ⊆ . An MKNF interpretation pair (, ) uniquely induces a consistent K-interpretation ( , ) where for each K ∈ KA():
K ∈ ( ∩ ) if ∀ ∈ , ( , ⟨, ⟩, ⟨, ⟩)(K) = t K ̸∈
if ∀ ∈ , ( , ⟨, ⟩, ⟨, ⟩)(K) = f
K ∈ ( ∖ ) if ∀ ∈ , ( , ⟨, ⟩, ⟨, ⟩)(K) = u Intuitively, contains K-atoms that are true and contains K-atoms that are possibly true (i.e. they are not false). We can acquire the set of false K-atoms by taking the complement of , e.g., = KA() ∖ and = KA() ∖ . When we use the letters , , and , we always mean sets of true, possibly true, and false K-atoms respectively.
We say that a K-interpretation ( , ) extends to an MKNF interpretation (, ) if ( , ) is consistent, OB, is consistent, and
(, ) = ({ | OB, |= }, { | OB, |= }) where is a first-order interpretation of () that is satisfies OB, or OB, respetively. This operation extends ( , ) to the ⊆ -maximal MKNF interpretation that induces ( , ).
We comment on how the relation induces and extends are related.
Remark 1. Let (, ) be an MKNF model of an MKNF knowledge base . A K-interpretation ( , ) that extends to (, ) exists, is unique and is the K-interpretation induced by (, ).
We say that an MKNF interpretation (, ) weakly induces a K-interpretation ( , ) if (, ) induces a K-interpretation ( * , * ) where ⊆ * and * ⊆ . Similarly, a Kinterpretation weakly extends to an MKNF interpretation (, ) if there exists an interpretation ( * , * ) that extends to (, ) such that ⊆ * , * ⊆ . Intuitively, we are leveraging the knowledge ordering u < t and u < f . A K-interpretation is weakly induced by an MKNF interpretation if that MKNF interpretation induces a K-interpretation that “knows more” than the original K-interpretation.
There are MKNF interpretations to which no K-interpretation extends, however, these are of
little interest; either OB, is inconsistent or (, ) is not maximal w.r.t. atoms that do not
appear in KA(). Similarly, there exist K-interpretations that extend to MKNF interpretations
that do not induce them. If this is the case, then the K-interpretation is missing some logical
consequences of the ontology and this should be corrected. We define the class of K-interpretations
that excludes the undesirable K-interpretations and MKNF interpretations from focus.
Definition 2.2. A K-interpretation ( , ) of an MKNF knowledge base is saturated if it can be
extended to an MKNF interpretation (, ) that induces ( , ). Equivalently, a K-interpretation
is saturated if ( , ) and OB, are consistent, OB, ̸|= for each K ∈ (KA() ∖ ) and
OB, ̸|= for each K ∈ (KA() ∖ ).
2We use ℘() to denote the powerset of , i.e., ℘() = { | ⊆ }
2.1. An Example Knowledge Base
Hybrid MKNF knowledge bases are equivalent to answer set semantics when the ontology is
empty. The definition of an MKNF program given is precisely the formulation of stable model
semantics [
Example 1. Let = (, ) be the following knowledge base
() = { ∨ ¬} (The definition of follows)
not K ← K ← not This knowledge base has two MKNF models ︁({︁ {, }, {, ¬}, {¬, ¬}}︁, {︁{, }}︁)︁
which induces the K-interpretation (∅, {K, K}) (, ) where = {︁{, ¬}, {, }}︁
which induces the K-interpretation ({K}, {K}) Above we have the answer set program that, without , admits three partial stable models. The ontology encodes an exclusive choice between the atoms and . The program allows for both and to be undefined. The ontology here is used as a filter to remove all interpretations where is false but is true.
The mixing of negation as failure and classical negation is not always straightforward. For example, let () = { ∨ } and = ∅. This knowledge base has just one MKNF model ︀( , )︀ where = {︁{, ¬}, {¬, }, {, }}︁
which induces the K-interpretation (∅, ∅) From the perspective of , which is only concerned with K-interpretations, all atoms are false. However, the interpretation {¬, ¬} is absent from the model which ensures that is still satisfied. Recall that () = K( ∨ ).
3-valued semantics allow for uncertainty to be encoded using an additional truth value, undefined. Well-founded semantics are a special case of 3-valued semantics and a well-founded model does not assign a K-atom to be true (resp. false) unless it is true (resp. false) in all 3-valued MKNF models.
We give a formal definition of well-founded semantics. have ′ ⊆ and ⊆ ′.
(, ) the well-founded model of (, ) if for every other MKNF model ( ′, ′) of we
Given a hybrid MKNF knowledge base with an MKNF model (, ), we call In general, a knowledge base may have several non-comparable minimal MKNF models and a well-founded model may not exist. While the minimality condition of MKNF minimizes interpretations according to the truth ordering f < u < t, a well-founded model is minimal w.r.t. the partial ordering u < t, u < f .
Crucially, a well-founded model contains information that must hold for all MKNF models
of a knowledge base. This property also holds for MKNF interpretations that contain a subset
of the knowledge found in the well-founded model. A polynomial algorithm will miss some
well-founded models or a well-founded model may not exist [
We now present a fixpoint operator that captures the 3-valued semantics of hybrid MKNF
knowledge bases. This operator builds directly upon prior work [
In the following, we use OB,, as shorthand for OB, ∪ {¬ | K ∈ } and we use ⊥ as an atom that is always false. The function ( ) can be any function ( ) : ∀, ′ ∈ ℘(KA()), ( ⊆ ′) ⇒ ( ( ) ⊆ ( ′)) To limit computational complexity, it is ideal for ( ) to be polynomial-time computable and for its image is restricted to elements of polynomial size w.r.t. syntactic measure of . This allows our operator that embeds to be polynomial. In the following, we use lfp (, ) to denote the least fixedpoint of the operator (, ).
2 =0 (, ) := (︁ ⋃︁ (, (KA() ∖ )), (KA() ∖ lfp (, )))︁ (, )( ) =
2 ︂( ⋃︁ (, ) ∖ 2 0(, ) := {K ∈ KA() | OB, |= } 1(, ) := {K | ∈ , K = ℎ(), +() ⊆ , K(− ()) ∩ = ∅} 0
(, )( ) := {K ∈ | ⊆ , ∈ ( ), OB,, ̸|= ⊥, OB,, |= ¬} 1
(, )( ) := {K ∈ | ∈ , ℎ() ∈ , K(− ()) ⊆ , (+() ∖ {K}) ⊆ } We use the letter to denote a parameter that contains true atoms, for possibly true atoms (either undefined or true) and for false atoms. and are used if the parameter could be a set of true or possibly true atoms. We give an intuitive explanation of each component of the operator.
• 0(, ): When is , everything that must be true as a consequence of the ontology is computed. When is , it returns everything that is possibly true as a consequence of the ontology. The second argument of the function is not used. • 1(, ): Similar to 0(, ), except that the consequences of are computed.
When (, ) = (, ) the not -atoms in the body of the rules are checked against atoms that are not in , i.e. they are false, whereas when (, ) = (, ), not -atoms are evaluated against atoms not present in , i.e., undefined atoms.
(, )( ): Computes atoms that are false as a consequence of the ontology. Uses • 0 atoms in that have been previously established as false to improve inferences. Subsets of must be checked for consistency with OB, because atoms may not necessarily be false in conjunction. To ensure monotonicity, the consistency of OB,, must be checked (which implies that OB, is consistent when (, ) is consistent.) If OB,, is consistent, then we will not gain any additional inferences by checking subsets of .
(, )( ): Finds rules where a single atom in the body has a value of undefined • 1 and the head of the rule is false. The single atom is set to be false. This rule relies on atoms that have been previously established as false to determine that the negative bodies of rules are satisfied. It would not be correct to use the complement of to perform this check.
It is sometimes convenient to use as an operator that takes and returns K-interpretations.
+(, ) = ( ′, KA() ∖ ′) where ( ′, ′) = (, KA() ∖ )
The operator is monotone w.r.t. the precision-ordering of K-interpretations, that is, the ordering on K-interpretations that embeds the ordering on logic values that ranks undefined beneath true and false.
Proposition 4.1. The +(, ) operator is monotone, i.e., for each (1, 1) and (2, 2) such that 1 ⊆ 2 and 2 ⊆ 1 we have (1′, 1′) = +(1, 1) (2′, 2′) = +(2, 2) 1′ ⊆ 1′, 2′ ⊆ 1′ Note that the above proposition holds for both consistent and inconsistent K-interpretations.
We now formally claim that the operator captures a sound approximation of models. Proposition 4.2. Let (, ) be an MKNF model of a knowledge base . For any K-interpretation (, ) that weakly extends to (, ), (, ) weakly induces +(, ).
If a well-founded model exists, then it weakly induces the K-interpretation (∅, KA()). We can obtain a more precise approximation of this well-founded model by iteratively applying + on (∅, KA()).
We can also easily check whether the K-interpretation computed by corresponds to the well-founded model.
Proposition 4.3. Let be an MKNF knowledge base with a well-founded model (, ). Extend the least fixedpoint of + to the MKNF interpretation ( ′, ′). We have ( ′, ′) = (, ) if ( ′, ′) |= ().
In some cases, we can compute the well-founded model by iteratively applying the + operator on (∅, KA()). To check whether the well-founded model can be computed using +, we can apply the operator until a fixpoint is reached then check whether it is the wellfounded model using Proposition 4.3. Even if the fixpoint is not the well-founded model, everything true or false in the fixpoint is also true and false respectively in the well-founded model due to Proposition 4.2.
The following example demonstrates basic application of the operator on a knowledge base. We demonstrate the more nuanced properties of the operator in the next section. Note that in this example, and subsequent examples, we omit K from atoms when describing K-interpretations. Example 2. Let = (, ) be the following MKNF knowledge base.
() = {( ⊃ ), ¬} (The definition of follows)
not K ← K ← not When we iteratively apply to (∅, ∅) we obtain the following sequence.
fails to compute as possibly true, it is added to the set of false atoms (∅, ∅) = (∅, {})
With false, the body of the first rule is true, so is derived (∅, {}) = ({}, {})
When is true, the ontology implies ({}, {}) = ({, }, {})
Finally, a fixpoint is reached ({, }, {}) = ({, }, {})
The operator (, ) provides significant improvements on the prior work. In particular, our operator makes better use of false atoms and can infer more negative consequences. In the coming section, we give general examples that demonstrate inference power improvements. While it remains to be shown whether these advancements may directly benefit practical use cases, the work here improves the theoretical basis for inferences that rely on classical negation and could be built upon to support practical use cases.
The work on fixpoint operators for 3-valued hybrid MKNF is split. The well-founded operator
from Ji, Liu and You [
In this section, we describe four operators in a uniform way to highlight their semantics diferences. While some restructuring of the operators was required to make meaningful comparisons, we believe the presentation below is faithful. The fixpoints of the operators are maintained. For ease of reference, we assign each operator a symbol (either , , , or ).
The alternating fixpoint operator from Knorr, Alferes, and Hitzler [
The well-founded operator from Ji, Liu and You [
The approximator defined by Liu and You [
Our well-founded operator defined in Section 4.
In the following, we define all four operators by prefixing each row with a set of these symbols. A definition for any of the operators can be reached by deleting all rows that do not contain the symbol corresponding to the operator.
⟩− (, ) := (︁ ⋃︁ (, (KA() ∖ )), (KA() ∖ lfp (, )))︁ • • • • ⟨, , , ⟨, , , ⟨, , , ⟨, , ,
2 =0 ︂(
2 =0 ⟨ ⟩− 0
(, )( ) := ∅ ⟨ ⟩− 0 ⟨ ⟩− 0 ⟨, ⟩− 1
(, )( ) := ∅ ⟩− (, )( ) = ⋃︁ (, ) ∖ ⟩− 1(, ) := {K | ∈ , K = ℎ(),
2 =0 +() ⊆ , K(− ()) ∩ = ∅} (, )( ) := {K ∈ | ( = {K} ∨ = ∅), ⊆ , OB,, |= ¬} (, )( ) := {K ∈ | OB, |= ¬} ⟨ ⟩− 0 (, )( ) := {K ∈ | ⊆ , ∈ ( ),
OB,, ̸|= ⊥, OB,, |= ¬} ⟨ ⟩− 1
(, )( ) := {K ∈ | ∈ , K = ℎ(), OB, |= ¬, ⟨ ⟩− 1 (, )( ) := {K ∈ | ∈ , ℎ() ∈ , K(− ()) ⊆ , (+() ∖ {K}) ⊆ , K(− ()) = ∅} (+() ∖ {K}) ⊆ }
In Table 1 we provide a high-level overview of the semantic diference between the operators that we will cover in the following examples.
Feature Description Ontology inferences use singleton sets of false atoms Ontology inferences with any subset of false atoms Rule unit propagation with positive rules Rule unit propagation with all rules See (3) See (3) See (4) See (4) Example A high-level overview of operator features is more precise.
Because 0
Minor diferences with how the operators deal with inconsistent information warrant us to limit our analysis to K-interpretations that are consistent and cannot be used to derive new information from the ontology. For this reason, we restrict our focus to saturated Kinterpretations.
Before we compare 0
(, )() for each operator, we note an ordering between them. = KA() ∖ , we have for all ⊆ Lemma 5.1. For any MKNF knowledge base and saturated K-interpretation (, ) where - 0 (, )() ⊆ - 0 (, )() ⊆ - 0 (, )() (, )() is computing atoms that should be false, a larger set of false atoms Example 3. The diference in the treatment of negation is the core distinction between and . In hybrid MKNF, negation as failure is looser than classical negation in the sense that OB, |= ¬ implies OB, |= not but the inverse does not necessarily hold. We compare 0 the , , and operators. In all three cases, we are propagating negative consequences from the (, ) across ontology.
The -0 The operator -0 (, ) operator only relies on true atoms to derive consequences with the ontology.
(, ) is slightly stronger and combines individual false atoms with the ontology. When = {K} is a singleton set we do not need to test whether OB,, is consistent. When we extend (, ) to an MKNF interpretation (, ), there must be a first-order interpretation in (, ) that assigns to be false. Otherwise, OB, would be inconsistent. When we allow to contain multiple K-atoms in -0 that the operator -0 to singleton subsets of like the following.
(, ) is equivalent to -0
(, ) when the filter function maps (, ), we must ensure that OB,, is consistent. Note ( ) := {{K} | K ∈ } ∪ {∅} In the coming example, we assume that ( ) returns the power set of . When we allow the set to be larger than a singleton, i.e., we provide the ontology with a conjunction of false atoms, it is possible that the ontology does not allow these atoms to be false in conjunction. While testing OB,, to be consistent would be suficient, this would result in a nonmonotonic operator.
We demonstrate these types of false inferences with a knowledge base. Let = (, ) be the following Note that the last three rules simply ensure that the K-atoms K, K, and K are present in KA(). Here, there is only one MKNF model and it induces the K-interpretation ({}, {}). The ontology encodes that a single atom must be true while all other atoms must be false. Consider the K-interpretation ({}, {, }). Each operator computes the following -(0{},{,})(∅) = -(0{},{,})(∅) = ∅
-(0{},{,})(∅) = {} When = {, } and = {}, we have OB,, |= ¬, thus the operator makes a more precise inference.
(, )( ), we note the following ordering.
Before we compare 1 Lemma 5.2. For any MKNF knowledge base and saturated K-interpretation ( , ) where = KA() ∖ , we have for all ⊆ - 1 (, )( )
(, )( ) ⊆ - 1
Like before, (1, )( ) is computing atoms that need to be false, therefore it is better for it to return larger sets.
Example 4. If the head of a rule must be false, then its body must also be false. If there is a single undefined atom in the positive body of such a rule preventing the body of the rule from being false, (, ) between the and the we can safely assign this atom to be false. We compare 1
(, ) function, the lone undefined atom must exist in a positive rule, operators. In the -1 (, ) function determines that is, a rule with an empty negative body. Additionally, the -1 the head of a rule to be false by checking if OB, entails it as false. As a result, false consequences (, ), cannot assist in determining that the computed by other parts of the operator, e.g. 0 head of the rule is false. Let = (, ) be the following knowledge base.
() = {( ∨ ) ∧ (¬ ∨ ¬) Here, ensures that either or is true, but not both. The program has a choice between K or K. If K is chosen, then both K and K must be true, which violates the ontology. This knowledge base has a single MKNF model that induces the K-interpretation ({, }, {, }). Consider the K-interpretation ({}, {, }). Both the -1 (, ) functions correctly (, ) and -1 compute that must be false. If we modify the final rule to be K ← K, K, not , the MKNF models are unchanged, but the operator fails to compute because the rule is no longer positive.
We now formally claim that our operator in Section 4 captures both the and operators. Proposition 5.1. For any MKNF knowledge base and K-interpretation (, ) where = KA() ∖ , we have - (, ) ⊑ - (, ) - (, ) ⊑ - (, ) Where (, ) ⊑ ( ′, ′) if ⊆ ′ and ⊆ ′.
Well-founded semantics play a vital role in eficient answer set solving. The ground, solve, check paradigm is still prevalent and grounders rely on well-founded semantics. In hybrid MKNF knowledge bases, well-founded semantics are intractable and well-founded models may not exist. Additional challenges must be overcome if we are to build efective grounders for hybrid MKNF. In this work, we improved upon the well-founded semantics for hybrid MKNF knowledge bases by capturing them with a well-founded fixpoint operator. We compared our operator with prior work and demonstrated the diferences to ultimately show that we expand the class of knowledge bases with known polynomial-time well-founded semantics. Because our operator performs well-founded propagation, it can also be used in conjunction with constraint propagation.
Future work could include using lookahead to achieve better unit propagation with rules. Currently, we rely on there being only a single undefined atom in the body of a rule, however, if there are two undefined atoms and assigning one to be false results in inconsistency, we may be able to safely assign the other atom as false.
We would like to acknowledge and thank Alberta Innovates and Alberta Advanced Education for their direct financial support of this research.