Conditional independence is a crucial concept supporting adequate modelling and eficient reasoning in probabilistics. In knowledge representation, the idea of conditional independence has also been introduced for specific formalisms, such as propositional logic and belief revision. In this paper, the notion of conditional independence is studied in the algebraic framework of approximation fixpoint theory. This gives a languageindependent account of conditional independence that can be straightforwardly applied to any logic with ifxpoint semantics. It is shown how this notion allows to reduce global reasoning to parallel instances of local reasoning. Furthermore, relations to existing notions of conditional independence are discussed and the framework is applied to normal logic programming.
language-independent investigations is the algebraic
approximation fixpoint theory (AFT) [
Due to the wide variety of formalisms studied mal logic programs, and it is shown that there are in knowledge representation, it is often beneficial strong connections with several existing works. yet challenging to study a concept in a language- Outline of the Paper: The necessary preliminaries independent manner. Indeed, such language- on logic programming (Section 2.1), lattices (Secindependent studies avoid having to define and in- tion 2.2 and approximation fixpoint theory (Section vestigate the same concept for diferent formalisms. 2.3) are introduced in Section 2. The concept of In recent years, a promising framework for such conditional independence of sub-lattices w.r.t. an operator is introduced and studied in Section 3.
S21epstteImntbeerrn2a–ti4o,n2a0l2W3o,rRkshhoodpeso,nGNreoencemonotonic Reasoning, This concept is applied to approximation operators $ jesse.heyninck@ou.nl (J. Heyninck) in Section 4. The usefulness of this theory is shown https://sites.google.com/view/jesseheyninck in Section 5, where it is applied to the semantics (J. Heyninck) of normal logic programs. Finally, related work 0000-0©0200223-3C8op2y5r-ig4h0t5fo2r (thJi.s pHaepyernbiynictks)authors. Use permitted under is discussed in Section 6, after which the paper is
Creative Commons License Attribution 4.0 International (CC BY concluded (Section 7).
CPWrEooUrckReshdoinpgs IhStpN:/c1e6u1r3-w-0s.o7r3g 4C.0E).UR Workshop Proceedings (CEUR-WS.org)
In this section, we recall the necessary basics of logic programming, abstract algebra and AFT.
(propositional) logic program is a finite set of rules of the form We assume a set of atoms and a language ℒ built up from atoms, conjunction ∧ and negation ¬ . A (a dlp, for short) ← , where (the rule’s (the rule’s head) is an atoms, and body) is a (propositional1) formula that may include the propositional constants T (representing truth), F (falsity), U (unknown), and C (contradictory information). A rule is called normal if its body is a conjunction of literals (i.e., atomic formulas or negated atoms). A program is normal if it consists only of normal rules; It is positive (or definite ) if there are no negations in the rules’ bodies. The set of atoms occurring in following four-valued bilattice:
is denoted . We use the ≤
F
T C U ≤ signed a value in {T, C} and atoms assigned a value in {T, U}. ⊆
is the set of 2 Interpretations are compared by the information order ≤ , where may be associated with a two-valued (or total) interpretation , in which for an atom , ( ) = T if a three-value (or consistent) interpretation, if ∈ and ( ) = F otherwise. We say that (, ) is Note that in consistent interpretations there are no ⊆ .
We now consider semantics for lp’s. First, given
a two-valued interpretation, an extension to dlp’s
of the immediate consequence operator for normal
programs [
Given a dlp and a two-valued inter ( ) = { ∈ |
← ∈ , (, )( ) = T}.
For a four-valued interpretation (, ), we define: ℐ (, ) = { | ← ∈ , (, )( ) ∈ {T, C}} ℐ (, ) = { | ← ∈ , (, )( ) ∈ {U, T}} IC (, ) = (ℐ (, ), ℐ (, )) heads of rules with true bodies.
Thus, denoting by 2 the powerset of , an operator on the lattice ⟨ 2 , ⊆⟩ that derives all is
Another common way of providing semantics to
dlp’s is by the following reduct [
We recall some necessary preliminaries on set theory and (sub-)lattices. A lattice is a partially ordered set = ⟨ℒ , ≤⟩ where every two elements , ∈ ℒ have a least upper ⊔ and a greatest lower bound valued interpretation of a program −F = T, −T = F, −U = U and −C = C). A fouris a pair (, ), where ⊆ is the set of the atoms that are as- ← ⋀︀ =1 ∧ ︀⋀ 1For simplicity and due to lack of space, we restrict ourselves to the propositional case. is a lower (upper) approximation of the true atoms. 2Somewhat skipping ahead, the intuition here is that ( ) ⊓ . A lattice is complete if every set ⊆ ℒ has bound (denoted ⊓
). a least upper (denoted ⊔ ) and a greatest lower ( (,
Let be a set, which we call the index set, and for each ∈ , let be a set. ⊗ ∈ is the following set of functions:
The product set = { | : →
s.t. ∀ ∈ : ( ) ∈ } ︁⋃ ample, for the sets 1 = {∅, { }} and 2 = {∅, { }}, (,
∈{1,2} contains, among others, and ′ with (1) = (2) = ∅ and ′(1) = ∅ and ′(2) = { }. For
If each is partially ordered by some ≤ , this induces the product order ≤⊗ on ⊗ ∈ : for all a finite set = {1, . . . , }, the product ⊗ ∈ is (isomorphic to) the cartesian product 1 × . . . × . operator by ( ≤⊗ if for all ∈ , ( ) ≤ ℒ 2, fixpoints of the stable operator ( ) are ≤ [16, Theorem 4]. Altogether, shown that if all ⟨ , ≤ ⟩ are (complete) lattices, then ⟨⊗ ∈ , ≤⊗⟩ is also a (complete) lattice. We ℒ call this the product lattice of the lattices .
⊆
︀⨂
We denote, for ∈ as ( ), and for
| For example, using 1 and 2 as in the ex a∈m ple above, ∅ × { }|1 = ∅ . Likewise, we denote by ⊗ . the element ∈ ⊗ s.t. | = for
= , ,
We now recall basic notions from approximation ifxpoint theory (AFT), as described by Denecker,
Given a lattice =
⟨ℒ , ≤⟩, we let 2 = 2 ⟨ℒ which ℒ , ≤ , ≤ ⟩ be the structure (called bilattice), in 2 = ℒ × ℒ
, and for every 1, 1, 2, 2 ∈ ℒ , operator ℒ
: ℒ → ℒ ∙ ( 1, 1) ≤ ( 2, 2) if 1 ≤ 2 and 1 ≥ 2,
An approximating operator ∙ ( 1, 1) ≤ ( 2, 2) if 1 ≤ 2 and 21 ≤ 2. → ℒ :
ℒ is an operator that maps 2 of an every approximation (, ) of an element to an approximation ( ′, ′) of another element ( ), thus approximating the behavior of the approximated operator .
Definition 3. (1)
is ≤ -monotonic, if when ( 1, 1) ≤ ( 2, 2), also ( 1, 1) ≤ ( 2, 2); (2) ing, if it is ≤ -monotonic and for any is approximat∈ ℒ , Let ℒ : ℒ → ℒ and : ℒ 2 (lfp( (., )), lfp( (, . )). We also denote the components lfp( (., )) and lfp( (, . ) of the stable )(, ) = )( ) respectively ( )( ).
Stable operators capture the idea of minimizing truth, since for any ≤ -monotonic operator on minimal fixpoints of we obtain the following notions:
2 be an approximating operator.
We call:
) a Kripke-Kleene fixpoint
of
if (,
) =
)); (2) (, ) a three-valued stable
fix= ⟨ℒ , ≤⟩, let
:
if (, ) = ( )(,
); (3) (,
valued stable fixpoints
(4) (,
) the well-founded fixpoint
of
if (,
) = (
minimal (three-valued) stable model fixpoint of .
It has been shown that every approximation
operator admits a unique ≤ -minimal stable fixpoint [
Conditional independence in an operator-based
setting is meant to formalize the idea that for the
application of an operator to a lattice consisting
3In some papers [
≤ -monotonic operator, i.e. a ≤
monotonic operator s.t. for every ,
( (,
), (,
)) for some :
ℒ
2 → ℒ . However, the
∈ ℒ , (,
) =
weaker condition we take here (taken from [
→ ⨂︀ ( ) = 1,3( 1 ⊗ 3) ⊗ 2,3( 2 ⊗ 3)|2. posed in two operators 1,3 : 1 ⊗
3 → 1 ⊗ 3 and 2,3 : 2 ⊗ 3 → 2 ⊗ 3 s.t. for any = 1 ⊗ 2 ⊗ 3 Definition 4.
Let
be an operator on the prodindependent
w.r.t. 3 according to uct lattice ⊗ ∈{1,2,3} . The lattices 1 and 2 are (in symbols: 1 ⊥⊥ 2 | 3) if there exist operators 1,3 : ⊗ ∈{1,3}ℒ → ⊗ ∈{2,3}ℒ s.t. for , ⊗ ∈{1,3}ℒ and 2,3 ⊗ ∈{2,3} ℒ →
∈ {1, 2}, ̸= , and for every that: ( ⊗ ⊗ 3)|, 3 = , 3( ⊗ 3). ⊗ 3 ∈ ℒ ⊗ ℒ 3 and for every ∈ ℒ it holds
Thus, two sub-lattices 1 and 2 are independent w.r.t. 3 according to
if, once we have full information about 3, information about 2 does not contribute anything in the application of when restricted to 1 (and vice versa).
Example 1. Consider the logic program atoms for infected, vaccinated and contact: 1 : inf(b) ← inf(a), cnct(a, b), not vac(b). 2 : inf(c) ← inf(a), cnct(a, c), not vac(c).
3 : inf(a)., 4 : cnct(a, b)., 5 : cnct(a, c).
Notice that, as soon as we know that infected(a). is the case, we can decompose the search for models into two independent parts, as can also be seen in the dependency graph in figure 1.
inf(b)
inf(c)
vac(b)
cnct(a, b)
inf(a)
cnct(a, c)
vac(c)
using example, not all semi-graphoid-properties [
We now show structural similarities with conditional independence known from probability theory: any 1 ⊗ 2 ⊗ 3 ∈
︀⨂ Fact 1. Let an operator on the product lattice ⊗ ∈{1,2,3}ℒ s.t. 1 ⊥⊥ 2 | 3 be given. Then for
∈{1,2,3} ℒ , it holds that: ( 1 ⊗ 2 ⊗ 3) = 1,2( 1 ⊗ 3) ⊗ 2,3( 2 ⊗ 3)|2
= 1,2( 1 ⊗ 3)|1 ⊗ 2,3( 2 ⊗ 3).
Furthermore, for any , ℒ , , ′ ∈ ℒ and 3 ∈ ℒ 3 it holds that: = 1, 2, ̸
= , ∈ ( ⊗ ⊗ 3)|, 3 = ( ⊗ ′ ⊗ 3)|, 3
However, this notion of conditional independence does show some diferences with conditional independence as known from probability theory. For satisfied. In more detail, whereas
symmetry (i.e. 1 ⊥⊥ 2 | 3 implies 2 viously satisfied, the properties of ⊥⊥ 1 | 3) is ob
decomposition (i.e. 1 and weak union (i.e. 1 ⊥⊥ 2 ⊗ 3 | ∅ implies
⊥⊥ 2 ⊗ 3 | ∅ implies 1 ⊥⊥ 2 | ∅) 1 ⊥⊥ 2 | 3) are not satisfied. composition, it should be noted that this property is undefined as we assume conditional independence over decompositions of the complete lattice. A violation of weak union is illustrated in the following
Example 2. Consider the logic program ; ← ¬ ; ← ¬ }. Note that 2{ } ⊥⊥IC
Yet it does not hold that 2{ } ⊥⊥IC 2{ } 2{, } = { ←
| ∅.
| 2{ }, as: IC ({ }) ∩ {, } IC ({, }) ∩ {, } = {, } ̸
= = { }
The reason for the failure of weak union is that we are not only interested in the behaviour of the operator
w.r.t. the conditionally independent sublattices 1 and 2, but also take into account the conditional pivot 3. This is to be contrasted with probabilistic conditional independence where the defining condition ( 1 |
3) = ( 1 | talks about 1. The reason that here conditional pivots are taken into account is that we are in
2, 3) only terested in fixpoints of an operator. It might be interesting to look at a weaker notion of conditional the conditional pivot in the output of the operator (and indeed, it is not hard to see that weak union is satisfied for such a notion), but due to our focus on fixpoints, we restrict attention to the stronger notion here.
We first note the following useful fact: Lemma 1. Let an operator on the product lattice ⊗ ∈{1,2,3}ℒ s.t. 1 ⊥⊥ 2 | 3 and ,
= 1, 2, ̸= We now undertake a study of the properties of Likewise, at least for monotonic operators over operators that respect conditional independencies. complete lattices, the least fixed points can be ob be given. Then 2,3( 2 ⊗ 3)|3 = 1,3( 1 ⊗ 3)|3. the complete product lattice ⊗ ∈{1,2,3} s.t. 1 ⊥⊥ ( 1 ⊗ 2 ⊗ 3) = 1,3( 1 ⊗ 3) ⊗ 2,3( 2 ⊗
3)|2 = Proof. As 1 ⊥⊥ 2 | 3, for any 2 ∈ ℒ 2, if |, 3 is a least fixed point of , 3 (for = 1, 2). ifxed point of . We show that 1⊗ 3 is a least fixed point of 1,3 (which sufices with symmetry). With sufices to show that for any fixed point of 1,3, ′1 ⊗ ′3
≥ 1 ⊗ 3. ′1 ⊗ ′3 = 1,3( ′1 ⊗ ′3). First, observe that ⊥2 ⊗ 3 ≤ ′2 ⊗ 3 for any ′2. By Lemma 1, 2,3( ′2 ⊗
′1 ⊗ ′3 1,3( 1 ⊗ 3)|1 ⊗ 2,3( 2 ⊗ 3), 1,3( 1 ⊗ 3)|3 = 2,3( 2 ⊗ 3)|3.
which implies
Fixpoints of an operator dence of 1 and 2 w.r.t. 3 can be obtained by combining the fixpoints of 1,3 and 2,3. Thus, the search for fixpoints can be split into two parallel problems with a smaller search space.
respecting indepen- Proposition 1, 1 ⊗ 3 = 1,3( 1 ⊗ 3). It thus 3 = ( 2 ⊗ 3).
Then
= ( ) if 1 ⊗ 3 = ( 1 ⊗ 3) and 2 ⊗ Proposition 1. Let an operator on the product ′3)|3 = 1,3( ′1 ⊗ ′3) = ′3 for any ′2 ∈ ℒ 2. Thus, and, as it is a ≤-monotonic operator (Proposition 2), a fixpoint is guaranteed to exist. Thus, there is suppose that 1 ⊗ 3 = ( 1 ⊗ 3) and 2 ⊗ 3 = ( 2 ⊗ 3). As 1 ⊥⊥ 2 | 3, ( 1 ⊗ 2 ⊗ 3) = Proof. For the ⇒-direction, suppose that = ( ). some ′2 ∈ ℒ 2 s.t. ( ′2 ⊗ ′3) = ′2 ⊗ ′3. This means Since 1 ⊥⊥ 2 |
3, , 3( ⊗ 3) = ( )|, 3 = |, 3 = ⊗ 3 (for = 1, 2). For the ⇐-direction, 1 ⊗ 2 ⊗ 3 ≤⊗ ′1 ⊗ ′2 ⊗ ′3, which on its turn that ′1 ⊗ ′2 ⊗ ′3 is a fixpoint of , which implies . lattice ⊗ ∈{1,2,3} s.t. 1 ⊥⊥ 2 | 3 be given. monotonic for = 1, 2. monotonic if , 3 : ℒ ⊗ ℒ 3 → ℒ ⊗ ℒ 3 is ≤,⊗3Proof. In what follows we let = {1, 2, 3}. For the ⇒-direction, suppose that and consider some 11 ⊗ 31 ≤⊗ is ≤⊗
-monotonic 1,3 12 ⊗ 32. Notice that ( 11 ⊗ 2 ⊗ 31
) ≤⊗ ( 12 ⊗ 2 ⊗ 32) for any 2 ∈ 2 (as is1≤,3⊗ -m1,o3(n o12to⊗nic)32. This means that 1,3( 11 ⊗ 31) ≤⊗ ) by definition of ≤⊗ and since 1 ⊥⊥ 2 | 3. For the ⇐-direction, suppose that , 3 are ≤-monotonic for = 1, 2. Consider some 1, 2 Then , 3( 1 | , 3) ≤⊗ ∈ , 3 ︀⨂ ∈{1,2,3} with 1 ≤⊗
2. , 3( 1
|, 3) for = 1, 2 which 2,3( |22,3)|2 by definition of implies 1,3( |11,3) ⊗ 2,3( |12,3)|2 ≤⊗ 1,3( 2
|1,3) ⊗ ∈{1,2,3} ℒ is ≤⊗- 4. Conditional Independence and ≤⊗. With conditional for Kripke-Kleene fixpoints, as well as any regular implies (by definition of
≤⊗), 1 ⊗ 3 ≤ ′1 ⊗ ′3.
Suppose now that |, 3 is a least fixed point of is a fixed point of . We show that for any fixed point ′ of , ′ ≥ 1 ⊗ 2 ⊗ 3. Indeed, with Proposition 1, ′|, 3 is a fixed point of , 3, which implies that ′|, 3 ≥ |, 3. By definition of
≤⊗,
The notion of conditional independence is immediately applicable to approximation operators. In this section, we will derive results on the modularisation of AFT-based semantics based on the results derived in the previous section.
As observed in previous work [
∈ ℒ 2, and we
will sometimes move between these two constructs
without further remarks [
As an approximation operator is a ≤ -monotonic operator, we immediately obtain that the search ifxpoints, can be split on the basis of conditional independence: Proposition 4. Let an approximation operator lfp(( (., ))1,3) ⊗
(lfp(( (., ))2,3)|2) (Proposition 3). view
of 1 ( )2,3( |2,3, |2,3)|2
⊥⊥ As ( (, ))
= for 2 any | 3),
( )1,3( |1,3, |1,3) ⊗ ∈
ℒ we see that (in over a bilattice of the product lattice ⊗ ∈{1,2,3}ℒ be given s.t. ℒ 1 ⊥⊥ ℒ 2 | ℒ 3. Then the following hold: (., )))1,3 = ( )1,3(., |1,3). Thus, lfp( (., )) = 2 2 2 As lfp(( )1,3)(., 1,3)) ⊗ lfp(( )2,3(., 2,3))|2. and ℒ 1 ⊥⊥ ℒ 2 | ℒ 3. given. Then ℒ 1 ⊥⊥ ℒ 2 | ℒ 32 if ℒ 1 ⊥⊥ ℒ 2 | ℒ 3 2 3 (for any 1 ∪ 2 ∪ 3 ⊆ ). 2 2
marginalisation As obtained by replacing in every rule ∈ occurrence of an atom ∈ by ⊥ . ⊆
Definition 5. Let a normal logic program and some be given.
We define
as the program every For example, { ← , , ¬ }{, } = { ← , ⊥, ⊤}.
Given a program inducing a conditional independence 1 ⊥⊥ 2 | 3, the marginalisation 2 gives use the immediate consequence operator for the sublattice 1 ∪ 3: Proposition 8. Let a normal logic program given for which is partitioned into 1 ∪ 2 ∪ 3 be , 3 , over a bilattice of the product lattice ⊗ ∈{1,2,3} be
In this section, we apply the theory developed in the previous section to normal logic programs. We can avoid clutter with a slight abuse of notation by writing 1 ⊥⊥ 2 | 3 to denote 2 1 ⊥⊥ℐ 2 2
| of a program w.r.t. a set of atoms: , 3 for = 1, 2. • (,
) is the Kripke-Kleene fixpoint of if ( |, 3, |, 3) is the Kripke-Kleene fixpoint of • (,
) is a fixpoint of ifxpoint of , 3 for = 1, 2.
if ( |, 3, |, 3) is a Proof. This is an immediate consequence of Propositions 1, 2 and 3.
We now turn our considerations to the stable operators. As a preliminary, we investigate the relation between an approximation operator and the lower and upper-bound component of this operator when it comes to respecting indpendencies. It turns out that the component operators and respect conditional independencies, and, vice-versa, that the respect of the two component operators of conditional independencies implies respect of these independencies by the approximation operator: Proposition 5. Let an approximation operator over a bilattice of the product lattice ⊗ ∈{1,2,3}ℒ be , 3(( , ) ⊗ ( 3, 3)) (for
2 ℒ 2 | ℒ 3
2 Proof. For the ⇒-direction, suppose that ℒ 12 ⊥⊥ ℒ ⊗ ℒ 3 s.t. (( 1, 1) ⊗ ( 2, 2) ⊗ ( 3, 3))|, 3 = , i.e. there are some , 3 : ℒ ⊗ ℒ 3 → = monotonic ([16, Proposition 6]), lfp( (., )) = ⊥⊥ 2 | 3.
As (., ) is ≤
⊥⊥ 22 | 32, with
Proposi- ℐ the proof.
We start by working out what the results in the previous sections mean for the semantics of logic programs. In particular, the search for supported, (partial) stable and well-founded models can be split up along conditionally independent sub-alphabets: < dep . and ⟨ 2, ∩ ( 2 × 2)⟩, and disconnected subgraphs ⟨ 1, ∩ ( 1 × 1)⟩ 2. for every ∈ 3 and ∈ ( = 1, 2), Corollary 1. Let a normal logic program be given Then 1 ⊥⊥ 2 | 3 holds. (for , for which is partitioned into 1 ∪ 2 ∪ 3 s.t. 1 ⊥⊥ 2 | 3. 1 ∪ 2 ∪ 3 is a supported (respectively three-valued stable) model of
if ∪ 3 is a supported (respectively three-valued stable) model of of | ∪ 3 (for = 1, 2). The well-founded model
can be obtained as ( 1 ∪ 2 ∪ 3, 1 ∪ 2 ∪ 3), where ( ∪ 3, ∪ 3) is the well-founded model of
We now make some observations on how to detect , conditional independencies in a logic program. We ifrst need some further preliminaries. The depen
= 1, 2 and ̸= .
Proof. Suppose the conditions of the proposition hold. Then for any ← ︀⋀ Δ ∧
︀⋀ {¬ | ∈ Θ}), (1) Δ∪Θ∩ ̸= ∅ implies
∈ (for = 1, 2), and (2) Δ∪Θ∪{ } ⊆ ∪ 3 (for = 1, 2).
From (1), it follows that †: ℐ ( 1 ∪ 2 ∪ 3)|3 =
Θ¬ (where Θ¬ = IC ℐ 1∪ 2 ( 3) for any
⊆ ( = 1, 2, 3). From (2) and †, it then follows that: ℐ ( 1∪ 2∪ 3)|, 3 = ( ∪ 3) for any ⊆ (
= 1, 2, 3) and This gives an example of how conditional indedency order for a logic program , ≤dep⊆ × , pendence can, at least partially, be identified on the is defined as ≤dep if there is some ∈
where is the head of and occurs in the body of . for more comprehensive, potentially even necessary, basis of the syntax of a logic program. The search (( ∖ ( 3) × ( ∖ ( 3)) consists of two sets of possible worlds (which is required to give a set 3 s.t. ⟨ ∖ 3,
∩ (( ∖ ( 3) × ( ∖ ( 3)) In this section, related work is discussed. We first
conditional independence 1 ⊥⊥ 2| 3. However, fixpoint theory [
The dependency graph, denoted DP( ) of is the
A first conjecture could be that, a suficient criterion fo 1 ⊥⊥ 2 | 3 is that 3 graphically separates 1 and 2, i.e. given DP( ) = ⟨ , ⟩
, consists of two disconnected subgraphs ⟨ 1, ∩ ( 1 × 1)⟩ and ⟨ 2,
∩ ( 2 × 1)⟩ induces the this conjecture is too naive: Example 3. Consider the program where 1 = { 1 ← ¬ 1; 1 ← ¬ 1; 2 = { 2 ← ¬ 2; 2 ← ¬
2; has the following dependency graph: ← 2}. This program = 1 ∪ 2 ← 1} and 1 1 e 2
2 ⊥ { 2, 2}|{ }, but this does not hold, as
We could conjecture the independency { 1, 1} ⊥
IC ({ 1, 2})|{ 1, 1, } ̸= IC ({ 1}) = { 1, } = { 1}.
A slightly more complicated graphical criterion is a suficient condition, though. In more detail, independency 1 ⊥⊥ 2 | 3 holds: if 3 graphically seperates 1 and 2 in DP( ), and if the program is stratified in a lower layer 3 and a higher layer 1 ∪ 2, then the conditional Proposition 9. Let a logic program
with DP( ) = ⟨ , ⟩ be given s.t. the following conditions hold 1. there is some 3 ⊆ s.t. ⟨ ∖ 3, ∩ criteria for identifying conditional independencies are an avenue for future work.
discuss Darwiche’s notion of conditional
independence [
Darwiche’s Logical Notion of Independence In
the context of classical logic, a notion of
conditional independence was proposed by Darwiche [
Darwiche assumes a database Δ (i.e. a set of propositional formulas), which is used as a background theory for inferences. The idea behind conditional independence is then that a database Δ sanctions the independence of two sets of atoms 1 and 2 conditional on a third set of atoms 3 if, given full information about 3, inferences about 1 are independent from any information about 2. In other words, given a set of formulas Δ and three disjoint sets of atoms 1, 2 and 3 be given, 1 ⊥⊥DΔ 2 | 3 if for every formula 1 based on 1, 2 based on 2 and complete conjunction of literals 3 based on 3 s.t. Δ ∪ { 3, 2} is consistent, the following holds: Δ ∪ { 3} |= 1 if
Δ ∪ { 2, 3} |= 1 Even though the application of our notion of conditional independence to operators ranging over an operator-based characterisation of propositional independent parts, whereas stratification allows to logic) is outside the scope of this paper, we can divide a lattice “vertically” in layers that incremennevertheless show a close connection between our tally depend on each other. It might be therefore notion of conditional independence and the one for- rather surprising that conditional independence can mulated by Darwiche by defining inference based be seen as a special case of stratification. on a logic program as follows (which gives rise to a special case of simple-minded output as known from First, we denote, for a product lattice ⨂︀
We first recall the definitions on stratifiability. .
, An input/output logics [20]): ⊆ s.t. ( ) = T, IC ( )( ) = T.
Definition 6. ,
Given a logic program based on , we define: |= if for every 1, 2 and formulas some 1 based on 1, some 2 based on 2 and a complete conjunction of literals 3 based on 3 be ( 1 Proposition 10. Let a program for which is partitioned into 1 ∪ 2 ∪ 3 s.t. 1 ⊥⊥ 2 | 3, 2 | 3. Suppose that 1, 2 Proof. For the ⇒-direction, suppose that 1 ⊥⊥
∈{1,2,3} and ∈ ︀⨂ is monotonic.
Proof. Suppose that the assumptions of this proposition holds. The ⇒-direction is immediate as |=
Suppose now that 3 ∧ 2 |= 1. Then for every 1 ∪ 2 ∪ 3 ⊆
s.t. 1 ∪ 2 ∪ 3( 3 ∧ 2) = T, IC ( 1 ∪ 2 ∪ 3)( 1) = T. Notice that there is a single 3 ⊆ 3 s.t. 3( 3) and 1 ∪ 2 ∪ 3( 3 ∧ 2) = T is independent of 1 (i.e. 1⋆ ∪ 2 ∪ 3( 3 ∧ 2) = T for any 1⋆ ⊆ 1). As 1 ⊥⊥ 2 | 3, IC ( 1 ∪ 2⋆ ∪ 3)|1,3 = IC ( 1 ∪
2⋆ ∪ 3)|1,3 for any 2⋆ ⊆ 2, we see that for any ′1 ⊆ 1, IC 2⋆ ∪ 3)|1( 1) = T, which implies 3 |= 1.
( ′1 ∪ Splitting Operators
A concept related to conditional independence studied in approximation fixpoint theory is that of straticfiation
[
←∼ ; layers { } , {, ←∼ ; ←∼ } can be stratified in the
}, { }. This concept was formulated
necker [
|{1,3}. that 11 ⊗ 31 = 12
⊗ 31. Then, as 1 ( 2)|{1,3} = 1,3( 11 ⊗ 31) = 1,3( 12 ⊗ 32 ) ⊥⊥ 2 | 3,
) =
For the ⇐-direction, suppose that is stratifiable over 1 ⊗ ( 2 ⊗ 3) and 2 ⊗ ( 1 ⊗ 3). Then we can define ( 1 ⊗⊗ 3) = ( 1 ⊗ 2 ⊗
3)|, 3 for any 2 ∈ 2 as ( 1 ⊗ 2 ⊗ 3)|, 3 = ( 1 ⊗ ′2 ⊗ 3)|, 3
On the other hand, stratification does not, in general, imply conditional independence, as conditional independence requires symmetry: ; { }, {, Example 4. Consider
←∼ }. Then dent from any of the other atoms.
can be stratified in the layers = { ←∼ ;
←∼ }, { } yet { } is not conditionally indepenDecomposing Logic Programs
A lot of eofrt has been devoted to the study of the paramterization of the computational complexity of various computational tasks using treewidth decompositions as a parameter [21]. These results show that the computational efort required in solving a problem is not a function of the overall size of the problem, but rather of certain structural parameters of the problem, i.e. the treewidth of a certain representabeen successfully applied to answer set programming [22]. In these works, the treewidth of the tree decomposition of the dependence graph DP( ) and incidence graph (which also contains vertices for inference based on logic programs: 3) and 2 ⊗ ( 1 ⊗ 3).
We can now show that our notion of conditional
independence implies Darwiche’s notion of condi- on the product lattice ⨂︀
tional independence, interpreted in the setting of 1 ⊥⊥ 2 | 3 if is stratifiable over 1 ⊗ ( 2 ⊗
∈{1,2,3} be given. Then
purely algebraically by Vennekens, Gilis and De- tion of the problem. These techniques have also
to those shown for stratified operators [
The only treewidth decomposition is the following: specific independence [ 29]. A third avenue for future decomposition would suggest the conditional independence { 1, 1} ⊥⊥
{ 2, 2} | { }, which does not hold. On the other hand, given that we phrased conditional independence semantically, some decompositions are not visible using the purely syntactic approach from [22]: Example 5. Let = { ← , ∼ ; ← ,
∼ ; ; ←∼ }, with the following dependency graph:
←∼
{, } {, }
{, } However (since the rules
← , ∼ and ← {, } ⊥⊥ {, } | ∅. , ∼ are never applicable), it can be verified that
Thus, the exact relationships between conditional independence and treewidth decompositions seem rather intricate and remain to be investigated.
Other operator-based formalisms have been analysed in terms of treewidth decompositions [23, 24].
A benefit of our operator-based approach is that all
results are purely algebraic and therefore
languageindependent, which means that applications to
specific formalisms are derived as straightforward
corollaries. Furthermore, the results for AFT-based
semantics, which subsume many KR-formalisms (see
[
Other Related Work
Conditional independence
has been investigated in several other logic-based
frameworks, such as (iterated) belief revision [
There exist several fruitful avenues for future work.
Firstly, we will investigate whether and how modularisation based on conditional independence can be used to obtain purely algebraic fixedparameter results. Secondly, we want to investigate related notions of independence, such as contextwork is a more extensive application of the theory to concrete formalisms, both in breadth (by applying the theory to further formalisms) and in depth (e.g. by investigating more syntactic methods to identify conditional independencies, and by evaluating the computational gain experimentally). revision, in:
ings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI22, 2022, pp. 2690–2696. doi:10.24963/ijcai. 2022/373, main Track.