The distribution semantics is an approach for integrating logic programming and probability theory that underlies many languages and has been successfully applied in many domains. When the program has function symbols, the semantics was defined for special cases: either the program has to be definite or the queries must have a finite number of finite explanations. In this paper we show that it is possible to define the semantics for all programs.
underlies many languages that combine logic programming with probability theory such as Probabilistic Horn Abduction, Independent Choice Logic, PRISM,
The definition of the distribution semantics can be given quite simply in the case of no function symbols in the program: a probabilistic logic program under the distribution semantics defines a probability distribution over normal logic programs called worlds and the probability of a ground query can be obtained by marginalizing the joint distribution of the worlds and the query. In the case the program has function symbols, however, this simple definition does not work as the probability of individual worlds is zero.
was proposed in [
programs, thus also for programs that have goals with an infinite number of
possibly infinite explanations. We do so by adapting the definition of the
wellfounded semantics in terms of iterated fixpoints of [
other languages under the distribution semantics, as there are linear transformations from one language to another that preserve the semantics.
The paper is organized as follows. Section 2 presents preliminary material on fixpoints and the well-founded semantics. Section 3 introduces the distribution semantics for programs without function symbols. Section 4 discusses the definition of the distribution semantics with function symbols in the case of finite set of finite explanations. Section 5 represents the main contribution of this paper and discusses the case of infinite set of infinite explanations. Finally, Section 6 concludes the paper. The proofs of the main results are reported in the
2
A relation on a set S is a partial order if it is reflexive, antisymmetric and transitive. In the following, let S be a set with a partial order ≤. a ∈ S is an upper bound of a subset X of S if x ≤ a for all x ∈ X. Similarly, b ∈ S is a lower bound of X if b ≤ x for all x ∈ X.
a ∈ S is the least upper bound of a subset X of X if a is an upper bound of X and, for all upper bounds a0 of X, we have a ≤ a0. Similarly, b ∈ S is the greatest lower bound of a subset X of S if b is a lower bound of X and, for all lower bounds b0 of X, we have b0 ≤ b. The least upper bound of X is unique, if it exists, and is denoted by lub(X). Similarly, the greatest lower bound of X is unique, if it exists, and is denoted by glb(X).
every subset X of L. We let > denote the top element lub(L) and ⊥ denote the bottom element glb(L) of the complete lattice L.
monotonic if T (x) ≤ T (y), whenever x ≤ y. We say a ∈ L is the least fixpoint of T if a is a fixpoint (that is, T (a) = a) and for all fixpoints b of T we have a ≤ b.
Proposition 1. Let L be a complete lattice and T : L → L be monotonic. Then T has a lest fixpoint, lfp(T ) and a greatest fixpoint gfp(T ).
r = h ← b1, . . . , bn, not c1, . . . , not cm (1) where h, b1, . . . , bn, c1, . . . , cm are atoms.
is called the Herbrand base and is denoted as BP .
lattice where the partial order ≤ is given by the subset relation ⊆. The least upper bound and greatest lower bound are defined as lub(X) = SI∈X I and glb(X) = TI∈X I. The bottom and top element are respectively ∅ and BP .
of BP and represent respectively the set of true and false atoms. The union of two three-valued interpretations hIT , IF i and hJT , JF i is defined as hIT , IF i ∪ hJT , JF i = hIT ∪JT , IF ∪JF i. The intersection of two three-valued interpretations hIT , IF i and hJT , JF i is defined as hIT , IF i ∩ hJT , JF i = hIT ∩ JT , IF ∩ JF i.
lattice where the partial order ≤ is defined as hIT , IF i ≤ hJT , JF i if IT ⊆ JT and IF ⊆ JF . The least upper bound and greatest lower bound are defined as lub(X) = SI∈X I and glb(X) = TI∈X I. The bottom and top element are respectively h∅, ∅i and hBP , BP i.
gram, i.e., it identifies a three-valued interpretation as the meaning of the
program. The WFS was given in [
Definition 1. For a normal program P , sets Tr and Fa of ground atoms, and a 3-valued interpretation I we define OpT rueIP (Tr ) = {a|a is not true in I; and there is a clause b ← l1, ..., ln in P , a grounding substitution θ such that a = bθ and for every 1 ≤ i ≤ n either liθ is true in I, or liθ ∈ Tr }; OpFalseIP (Fa) = {a|a is not false in I; and for every clause b ← l1, ..., ln in P and grounding substitution θ such that a = bθ there is some i (1 ≤ i ≤ n) such that liθ is false in I or liθ ∈ Fa}.
In words, the operator OpT rueIP extends the interpretation I to add the new
atomic facts that can be derived from P knowing I, while OpFalseP adds the new
I
negations of atomic facts that can be shown false in P by knowing I. OpT rueIP
and OpFalseIP are both monotonic [
Definition 2 (Iterated Fixed Point). For a normal program P , let IFP P :
Int3 → Int3 be defined as IFP P (I) = I ∪ hlfp(OpT rueIP ), gfp(OpFalseIP )i.
IFP P is monotonic [
We present the distribution semantics for the case of ProbLog [
probabilistic facts.
fact F . It is represented with the triple (F, θ, i) where i ∈ {0, 1}. A set κ of atomic choices is consistent if it does not contain two atomic choices (F, θ, i) and (F, θ, j) with i 6= j (only one alternative is selected for a ground probabilistic fact). The function consistent(κ) returns true if κ is consistent. A composite choice κ is a consistent set of atomic choices. The probability of composite choice κ is P (κ) = Q(Fi,θ,1)∈κ pi Q(Fi,θ,0)∈κ 1 − pi where pi is the probability of the i-th probabilistic fact Fi. A selection σ is a total composite choice, i.e., it contains one atomic choice for every grounding of each probabilistic fact. A world wσ is a logic program that is identified by a selection σ. The world wσ is formed by including the atom corresponding to each atomic choice (F, θ, 1) of σ.
The probability of a world wσ is P (wσ) = P (σ). Since in this section we are assuming programs without function symbols, the set of groundings of each probabilistic fact is finite, and so is the set of worlds WP . Accordingly, for a ProbLog program P, WP = {w1, . . . , wm}. Moreover, P (w) is a distribution over worlds: Pw∈WP P (w) = 1. We call sound a program for which every world has a two-valued well-founded model. We consider only sound programs, as the uncertainty should be handled by the choices rather than by the semantics of negation.
probability of q given a world w as: P (q|w) = 1 if q is true in w and 0 otherwise.
of q can thus be computed by summing out the worlds from the joint distribution of the query and the worlds: P (q) = Pw P (q, w) = Pw P (q|w)P (w) = Pw|=q P (w). 4
defines a world is countably infinite and there is an uncountably infinite number of worlds. In this case, the probability of each individual world is zero since it is the product of infinite numbers all smaller than one. So the semantics of Section
p(0) ← u(0). t ← ¬s. F1 = a :: u(X). p(s(X)) ← p(X), u(X). s ← r, ¬q. F2 = b :: r.
q ← u(X).
The set of worlds is infinite and uncountable. In fact, each world can be put in a one to one relation with a selection and a selection can be represented as a countable sequence of atomic choices of which the first involves fact F2, the second F1/{X/0}, the third F1/{X/s(0)} and so on. The set of selections can be shown uncountable by Cantor’s diagonal argument. Suppose the set of selections is countable. Then the selections could be listed in order, suppose from top to bottom. Suppose the atomic choices of each selection are listed from left to right. We can pick a composite choice that differs from the first selection in the first atomic choice (if (F2, ∅, k) is the first atomic choice of the first selection, pick (F2, ∅, 1 − k)), from the second selection in the second atomic choice (similar to the case of the first atomic choice) and so on. In this way we have obtained a selection that is not present in the list because it differs from each selection in the list for at least an atomic choice. So it is not possible to list the selections in order.
We now present the definition of the distribution semantics for programs with
function symbols following [
Definition 3. [11, Section 3.1] The set Ω of subsets of W is a σ-algebra on the set W iff (σ-1) W ∈ Ω; (σ-2) Ω is closed under complementation, i.e., ω ∈ Ω → (W \ ω) ∈ Ω; and (σ-3) Ω is closed under countable union, i.e., if ωi ∈ Ω for i = 1, 2, . . . then Si ωi ∈ Ω.
tribution semantics for programs with function symbols, not every subset of W need be present in Ω.
Definition 4. [
Definition 5. [11, Section 3.1] The set Ω of subsets of W is an algebra on the set W iff it respects conditions (σ-1), (σ-2) and condition (a-3): Ω is closed under finite union, i.e., ω1 ∈ Ω, ω2 ∈ Ω → (ω1 ∪ ω2) ∈ Ω
Definition 6. Given a sample space W and an algebra Ω of subsets of W, a finitely additive probability measure is a function μ : Ω → R that satisfies axioms (μ-1) and (μ-2) of Definition 4 and axiom (m-3): μ is finitely additive, i.e., ω1 ∩ ω2 = ∅ → μ(ω1 ∪ ω2) = μ(ω1) + μ(ω2) for all ω1, ω2 ∈ Ω.
define the set of worlds ωκ compatible with a composite choice κ as ωκ = {wσ ∈
without function symbols P (κ) = Pw∈ωκ P (w).
Given a set of composite choices K, the set of worlds ωK compatible with K is ωK = Sκ∈K ωκ. Two composite choices κ1 and κ2 are incompatible if their union is not consistent. A set K of composite choices is pairwise incompatible if for all κ1 ∈ K, κ2 ∈ K, κ1 6= κ2 implies that κ1 and κ2 are incompatible.
worlds or not, obtaining pairwise incompatible sets of composite choices is an important problem. This is because the probability of a pairwise incompatible set K of composite choices is defined as P (K) = Pκ∈K P (κ) which is easily computed. Two sets K1 and K2 of finite composite choices are equivalent if they correspond to the same set of worlds: ωK1 = ωK2 .
One way to assign probabilities to a set K of composite choices is to construct an equivalent set that is pairwise incompatible; such a set can be constructed through the technique of splitting. More specifically, if F θ is an instantiated fact and κ is a composite choice that does not contain an atomic choice (F, θ, k) for any k, the split of κ on F θ is the set of composite choices Sκ,F θ = {κ ∪ {(F, θ, 0)}, κ ∪{(F, θ, 1)}}. It is easy to see that κ and Sκ,F θ identify the same set of possible worlds, i.e., that ωκ = ωSκ,F θ , and that Sκ,F θ is pairwise incompatible.
Theorem 1 (Existence of a pairwise incompatible set of composite choices [
1. removing dominated elements: if κ1, κ2 ∈ K and κ1 ⊂ κ2, let K0 =
K \ {κ2}.
In both cases ωK = ωK0 . If we repeat this two operations until neither is
applicable we obtain a splitting algorithm that terminates because K is a finite
set of composite choices. The resulting set K0 is pairwise incompatible and is
equivalent to the original set.
♦
Theorem 2 (Equivalence of the probability of two equivalent pairwise
incompatible finite set of finite composite choices [
measure μ : ΩP → [
choices are removed obtaining K. Since the possible choices of the atomic choices are finite, so is K. Finally, condition (a-3) holds since the union of ωK1 with ωK2 is equal to ωK1∪K2 for the definition of ωK .
The corresponding measure μ is defined by μ(ωK ) = P (K0) where K0 is a pairwise incompatible set of composite choices equivalent to K. hWP , ΩP , μi is a finitely additive probability space according to Definition 6 because μ(ω{∅}) = 1, μ(ωK ) ≥ 0 for all K and if ωK1 ∩ ωK2 = ∅ and K10 (K20) is pairwise incompatible and equivalent to K1 (K2), then K10 ∪ K20 is pairwise incompatible and μ(ωK1 ∪ ωK2 ) =
X κ∈K10∪K20
P (κ) =
X κ1∈K10
P (κ1) +
X κ2∈K20
P (κ2) = μ(ωK1 ) + μ(ωK2 ).
Given a query q, a composite choice κ is an explanation for q if ∀w ∈ ωκ : w |= q.
belongs to ωK Definition 7. For a probabilistic logic program P, the probability of a ground atom q is given by P (q) = μ({w|w ∈ WP , w |= q}).
Example 2. Consider the program of Example 1. The set K = {κ} with κ = {(F1, {X/0}, 1), (F1, {X/s(0)}, 1)} is a pairwise incompatible finite set of finite explanations that are covering for the query p(s(0)). Definition 7 therefore applies, and P (p(s(0))) = P (κ) = a2 5
of the covering set of explanations and of each explanation for a query q. Example 3. In Example 1, the query s has the pairwise incompatible covering set of explanations Ks = {κs0, κs1, . . .} with
κis = {(F2, ∅, 1), (F1, {X/0}, 1), . . . , (F1, {X/si−1(0)}, 1), (F1, {X/si(0)}, 0)} where si(0) is the term where the functor s is applied i times to 0. So Ks is countable and infinite. A covering set of explanation for t is Kt = {{(F2, ∅, 0)}, κt} where κt is the infinite composite choice
κt = {(F2, ∅, 1), (F1, {X/0}, 1), (F1, {X/s(0)}, 1), . . .}
Lemma 3 ΩP is a an σ-algebra over WP .
Proof: (σ-1) is true as in the algebra case. To see that the complement ωKc of ωK is in ΩP , let us prove by induction that the dual K of K is a countable set of countable composite choices and then that ωKc = ωK . In the base case, if K1 = {κ1}, then we can obtain K1 by picking each atomic choice (F, θ, k) of κ1 and inserting in K1 the composite choice {(F, θ, 1 − k)}. As there is a finite or countable number of atomic choices in κ1, K1 is a finite or countable set of composite choices each with one atomic choice.
In the inductive case, assume that Kn−1 = {κ1, . . . , κn−1} and that Kn−1 is a finite or countable set of composite choices. Let Kn = Kn−1 ∪ {κn} and Kn−1 = {κ01, κ02, . . .}. We can obtain Kn by picking each κ0i and each atomic choice (F, θ, k) of κn. If (F, θ, k) ∈ κ0 , then discard κ0 , else if (F, θ, k0) ∈ κ0 i i i with k0 6= k, insert κ0i in Kn. Otherwise generate the composite choice κ0i0 where κ0i0 = κ0i ∪ {(F, θ, 1 − k)} and insert it in Kn. Doing this for all atomic choices (F, θ, k) in κn generates a finite set of composite choices if κn is finite and a countable number if κn is countable. Doing this for all κ0i we obtain that Kn is a countable union of countable sets which is a countable set [14, page 3]. ωKc = ωK because all composite choices of K are incompatible with each world of ωK , as they are incompatible with each composite choice of K. So ωKc ∈ ΩP . (σ-3) is true as in the algebra case. ♦
We can see K as limn→∞ Kn where Kn = {κ1, . . . , κn}. Each Kn is a finite set of composite choices and we can compute an equivalent finite pairwise incompatible set of composite choices Kn0. For each Kn0 we can compute the probability P (Kn0), noting that the probability of infinite composite choices is 0.
of a series. Moreover, it can be shown that P (Kn0−1) ≤ P (Kn0) so the series has non-negative terms. Such a series converges if the sequence of partial sums is bounded from above [15, page 92]. Since P (Kn0) is bounded by 1, the limit limn→∞ P (Kn0) exists. So we can define measure μ as μ(ωK ) = limn→∞ P (Kn0). Theorem 4 hWP , ΩP , μi is a probability space according to Definition 4. Proof: (μ-1) and (μ-2) hold as for the finite case and for (μ-3) let O = {ωL1 , ωL2 , . . .} be a countable set of subsets of ΩP such that the ωLi s are pairwise disjoint. Let L0i be the pairwise incompatible set equivalent to Li and let L be Si∞=1 L0 . Since the ωLi s are pairwise disjoint, then L is pairwise incomi patible. ΩP is a σ-algebra, so L is countable. Let L be {κ1, κ2, . . .} and let Kn0 be {κ1, . . . , κn}. Then μ(O) = limn→∞ P (Kn0) = limn→∞ Pκ∈Kn0 P (κ) = Pκ∈L P (κ). Since L = Si∞=1 L0i, by rearranging the terms in the last summation we get μ(O) = Pκ∈L P (κ) = Pn∞=1 P (L0n) = Pn∞=1 μ(ωLn ). ♦
again given by P (q) = μ({w|w ∈ WP , w |= q}). If q has a countable set K of explanations such that K is covering then {w|w ∈ WP ∧ w |= q} = ωK ∈ ΩP and we say that P (q) is well-defined for the distribution semantics. A program
well-defined.
Example 4. Consider Example 3. Since the explanations in Ks are pairwise incompatible the probability of s can be computed as
P (s) = b(1 − a) + ba(1 − a) + ba2(1 − a) + . . . = b(1 − a) 1 − a = b. since the sum is a geometric series. Kt is also pairwise incompatible and P (κt) = 0 so P (t) = 1 − b + 0 = 1 − b which is what we intuitively expect.
K2 of K1 and K2 as K1 ⊗ K2 = {κ1 ∪ κ2|κ1 ∈ K1, κ2 ∈ K2, consistent(κ1 ∪ κ2)}
ator. Differently from [
Definition 8 (Parameterized two-valued interpretations). A parameterized positive two-valued interpretation Tr of a ground probabilistic logic program P with and atoms BP is a set of pairs (a, Ka) with a ∈ atoms and Ka a set of composite choices. A parameterized negative two-valued interpretation Fa of a ground probabilistic logic program P with atoms BP is a set of pairs (a, K¬a) with a ∈ BP and K¬a a set of composite choices.
tial order is defined as I ≤ J if ∀(a, Ka) ∈ I, (a, La) ∈ J : ωKa ⊆ ωLa . The least upper bound and greatest lower bound always exist and are lub(X) = {(a, S(a,Ka)∈I,I∈X Ka)|a ∈ BP } and glb(X) = {(a, N(a,Ka)∈I,I∈X Ka)|a ∈ BP }.
BP }.
Definition 9 (Parameterized three-valued interpretation). A parameterized three-valued interpretation I of a ground probabilistic logic program P with atoms BP is a set of triples (a, Ka, K¬a) with a ∈ BP and Ka and K¬a sets of composite choices.
tial order is defined as I ≤ J if ∀(a, Ka, K¬a) ∈ I, (a, La, L¬a) ∈ J : ωKa ⊆ ωLa and ωK¬a ⊆ ωL¬a . The least upper bound and greatest lower bound always exist and are lub(X) = {(a, S(a,Ka,K¬a)∈I,I∈X Ka, S(a,Ka,K¬a)∈I,I∈X K¬a)|a ∈ BP } and glb(X) = {(a, N(a,Ka,K¬a)∈I,I∈X Ka, N(a,Ka,K¬a)∈I,I∈X K¬a)|a ∈ BP }. The top element > is {(a, {∅}, {∅})|a ∈ BP }, the bottom element ⊥ is {(a, ∅, ∅)|a ∈ BP }.
Definition 10. For a ground program P, a two-valued parametrized positive interpretation Tr with pairs (a, La), a two-valued parametrized negative interpretation Fa with pairs (a, M¬a) and a three-valued parametrized interpretation I with triples (a, Ka, K¬a), we define OpT rueCP (Tr ) = {(a, L0a)|a ∈ BP } where I L0a = S{{(a, ∅, 1)}}
a←b1,...,bn,¬c1,...,cm∈R((Lb1 ∪ Kb1 ) ⊗ . . . ⊗(Lbn ∪ Kbn ) ⊗ K¬c1 ⊗ . . . ⊗ K¬cm ) if a ∈ F if a ∈ BP \ F OpFalseC P (Fa) = {(a, Ma0 )|a ∈ BP } where
I M ¬0a = {N{(a, ∅, 0)}}
a←b1,...,bn,¬c1,...,cm∈R((M¬b1 ⊗ K¬b1 ) ∪ . . . ∪(M¬bn ⊗ K¬bn ) ∪ Kc1 ∪ . . . ∪ Kcm ) if a ∈ F if a ∈ BP \ F Proposition 5 OpT rueCP and OpFalseC IP are monotonic.
I Since OpT rueCIP and OpFalseC IP are monotonic, they have a least fixpoint and a greatest fixpoint.
Definition 11 (Iterated Fixed Point). For a ground program P, let IFPC P be defined as IFPC P (I) = {(a, Ka, K¬a)|(a, Ka) ∈ lfp(OpT rueCIP ), (a, K¬a) ∈ lfp(OpFalseC IP )}.
Proposition 6 IFPC P is monotonic.
the smallest ordinal such that IFPC P ↑ δ = WFMC (P). We refer to δ as the depth of P. Theorem 7 For a ground probabilistic logic program P with atoms BP , let Kaα and Kα
¬a be the formulas associated with atom a in IFPC P ↑ α. For every atom a and total choice σ, there is an iteration α0 such that for all α > α0 we have: Theorem 8 For a ground probabilistic logic program P, let Kaα and K¬αa be the formulas associated with atom a in IFPC P ↑ α. For every atom a and every iteration α, Kaα and K¬αa are countable sets of countable composite choices.
that is covering and the probability measure is well defined. Moreover, since the program is sound, for all atoms a, ωKaδ = ωKc¬δa where δ is the depth of the program, as in each world a is either true or false.
Comparison with Sato and Kameya’s Definition that
of finite distributions. Let F be {F1, F2, . . .} and let Xi be a random variable associated to Fi whose domain is {0, 1}.
The finite distributions P (n)(X1 = k1, . . . , Xn = kn) for n ≥ 1 must be such
P 0 ≤ P (n)(X1 = k1, . . . , Xn = kn) ≤ 1 Pk1,..P.,kn PP(n)(X1 = k1, . . . , Xn = kn) = 1 Pkn+1 PP(n+1)(X1 = k1, . . . , Xn+1 = kn+1) = PP(n)(X1 = k1, . . . , Xn = kn) (2)
the compatibility condition that there exists a probability space (WP , ΨP , η) where η is a probability measure on ΨP , the minimal σ-algebra containing open sets of WP such that for any n, η(X1 = k1, . . . , Xn = kn) = PT(n)(X1 = k1, . . . , Xn = kn). (3) P (n)(X1 = k1, . . . , Xn = kn) is defined as P (n)(X1 = k1, . . . , Xn = kn) =
P P p1 . . . pn where pi is the annotation of alternative ki in fact Fi. This definition clearly satisfies the properties in (2). P (n)(X1 = k1, . . . , Xn = kn) is then exP tended to a probability measure over BP .
symbols coincides for definite programs with the one given above.
To show that the two definition coincide, we conjecture that ΨP = ΩT . Moreover, X1 = k1, . . . , Xn = kn is equivalent to the set of composite choices K = {{(F1, ∅, k1), . . . , (Fn, ∅, kn)}} and μ(ωK ) gives p1 . . . pn which satisfies equation (3). 6
iterated fixpoint operator that allowed us to prove that the semantics is well
defined for all programs. The operator we have presented is also interesting from
an inference point of view, as it can be used for forward inference similarly to
[
Proposition 5 OpT rueCIP and OpFalseC IP are monotonic.
Proof: Let us consider OpT rueCIP . We have to prove that if Tr 1 ≤ Tr 2 then OpT rueCIP (Tr 1) ≤ OpT rueCP (Tr 2). Tr 1 ≤ Tr 2 means that ∀(a, La) ∈
I
I and (a, Ma0 ) the elements of OpT rueCP (Tr 2). We have to prove that L0a ⊆ Ma0
I
If a ∈ F then L0a = Ma0 = {{(a, θ, 1)}}. If a ∈ BP \ F , then L0a and Ma0 have the same structure. Since ∀b ∈ BP : Lb ⊆ Mb, then L0a ⊆ Ma0
We can prove similarly that OpFalseC IP is monotonic. ♦ Proposition 6 IFPC P is monotonic.
I1 ≤ I2 means that ∀(a, La, L¬a) ∈ I1, (a, Ma, M¬a) ∈ I2 : La ⊆ Ma, L¬a ⊆ eMm¬ean.tsLeotf (IaF,PLC0a,PL(0¬Ia2)).bWeethheaveelemtoenptrsovoef tIhFaPtCLP0a(⊆I1)Maa0ndan(da,LM0¬aa0 ,⊆M ¬M0a¬)0at.hTeheilsfollows from the montonicity of OpT rueCIP1 and OpFalseC IP2 in I1 and I2 respectively, which can be proved as in Proposition 5. ♦ Lemma 9 For a ground probabilistic logic program P with probabilistic facts F , rules R and atoms BP , let Laα be the formula associated with atom a in OpT rueCIP ↑ α. For every atom a, total choice σ and iteration α, we have: wσ ∈ ωLaα → WFM (wσ|I) |= a where wσ|I is obtained by adding to wσ the atoms a for which (a, Ka, K¬a) ∈ I and wσ ∈ Ka as facts and by removing all the rules with a in the head for which (a, Ka, K¬a) ∈ I and wσ ∈ K¬a.
for all β < α and let us prove it for α. If α is a successor ordinal, then it is easily verified for a ∈ F . Otherwise assume wσ ∈ ωLaα where
((Lbα1−1∪Kb1 )⊗. . . ⊗(Lbαn−1∪Kbn )⊗K¬c1 ⊗. . .⊗K¬cm ) Laα =
[ a←b1,...,bn,¬c1,...,cm∈R This means that there is rule a ← b1, . . . , bn, ¬c1, . . . , cm ∈ R such that wσ ∈ ωLα−1∪Kbi for i = 1, . . . , n and wσ ∈ ωK¬cj for j = 1 . . . , m. By the inducbi tive assumption and because of how wσ|I is built then WFM (wσ|I) |= bi and WFM (wσ|I) |= ¬cj so WFM (wσ|I) |= a.
Laα = lub({Laβ|β < α}) = [ La
β β<α If wσ ∈ ωLaα then there must exist a β < α such that wσ ∈ ωLaβ . By the inductive assumption the hypothesis holds. ♦ Lemma 10 For a ground probabilistic logic program P with probabilistic facts F , rules R and atoms BP , let M α
¬a be the set of composite choices associated with atom a in OpFalseC IP ↓ α. For every atom a, total choice σ and iteration α, we have:
wσ ∈ ωM¬a → WFM (wσ|I) |= ¬a where wσ|I is built as in Lemma 9.
♦ (4) (5) Lemma 11 For a ground probabilistic logic program P with probabilistic facts F , rules R and atoms BP , let Kaα and Kα ¬a be the formulas associated with atom a in IFPC P ↑ α. For every atom a, total choice σ and iteration α, we have: wσ ∈ ωKaα → WFM (wσ) |= a wσ ∈ ωK¬αa → WFM (wσ) |= ¬a Proof: Let us first prove that for all α, WFM (wσ) = WFM (wσ|IFPC P ↑ α).
ordinal. Consider an atom b. If wσ 6∈ ωKbα and wσ 6∈ ωK¬αb then the rules for b in wσ and wσ|IFPC P ↑ α are the same. If wσ ∈ ωKbα then b is a fact in wσ|IFPC P ↑ α but, according to Lemma 9, WFM (wσ|IFPC P ↑ (α−1)) |= b. For the inductive hypothesis WFM (wσ) |= b so b has the same truth value in WFM (wσ) and WFM (wσ|IFPC P ↑ α). Similarly, if wσ ∈ ωK¬αb , then WFM (wσ) |= ¬b and b has the same truth value in WFM (wσ) and WFM (wσ|IFPC P ↑ α). So overall WFM (wσ) = WFM (wσ|IFPC P ↑ α).
If α is a limit ordinal, then Kbα = Sβ<α Kbβ and K¬αb = Sβ<α Kbβ. So if wσ ∈ ωKbα there is a β such wσ ∈ ωKβ and for the inductive hypothesis WFM (wσ) |= b b so b has the same truth value in WFM (wσ) and WFM (wσ|IFPC P ↑ α). Similarly if wσ ∈ ωK¬αb .
α a successor ordinal. Since (a, Kaα) ∈ lfp(OpT rueCIPFPC ↑(α−1)), by Lemma 9 wσ ∈ ωKaα → WFM (wσ|IFPC P ↑ (α − 1)) |= a Since WFM (wσ|IFPC P ↑ (α − 1)) = WFM (wσ), (4) is proved.
Since (a, K¬αa) ∈ gfp(OpFalseC IPFPC P↑(α−1)), by Lemma 10
wσ ∈ ωK¬αa → WFM (wσ|IFPC P ↑ (α − 1)) |= ¬a Since WFM (wσ|IFPC P ↑ (α − 1)) = WFM (wσ), (5) is proved.
If α is a limit ordinal, Kaα = Sβ<α Kaβ and K¬αa = Sβ<α Kaβ. If wσ ∈ ωKaα there is a β such that wσ ∈ ωKbα and by the inductive hypothesis (4) is proved.
♦ Lemma 12 For a ground probabilistic logic program P with probabilistic facts F , rules R and atoms BP , let Kaα and Kα ¬a be the formulas associated with atom a in IFPC P ↑ α. For every atom a, total choice σ and iteration α, we have: a ∈ IFP wσ ↑ α → wσ ∈ Kaα ¬a ∈ IFP wσ ↑ α → wσ ∈ K¬αa
a ∈ IFP wσ ↑ (α − 1) → wσ ∈ Kaα−1 ¬a ∈ IFP wσ ↑ (α − 1) → wσ ∈ K¬αa−1 Let us perform transfinite induction on the iterations of OpTrueIPFPC P↑(α−1). Let us consider a successor ordinal δ: assume that and prove that
a ∈ OpTrueIwFσPwσ ↑(α−1) ↑ (δ − 1) → wσ ∈ Lδa−1 ¬a ∈ OpFalseIwFσPwσ ↑(α−1) ↓ (δ − 1) → wσ ∈ M¬δ−a1 a ∈ OpTrueIwFσPwσ ↑(α−1) ↑ δ → wσ ∈ La δ ¬a ∈ OpFalseIwFσPwσ ↑(α−1) ↓ δ → wσ ∈ M¬δa
For other atoms a, a ∈ OpTrueIwFσPwσ ↑(α−1) ↑ δ means that there is a rule a ← b1, . . . , bn, ¬c1, . . . , cm such that for all i = 1, . . . , n bi ∈ OpTrueIwFσPwσ ↑(α−1) ↑ (δ − 1) and for all j = 1, . . . , m ¬cj ∈ IFP wσ ↑ (α − 1). For the inductive hypothesis ∀i : wσ ∈ Lbδi−1 ∨ wσ ∈ Kbαi−1 and ∀j : wσ ∈ K¬αc−j1 so, for the definition of OpTrueIwFσPwσ ↑(α−1), wσ ∈ Lδa. Analogously for ¬a.
If δ is a limit ordinal, then Lδa = Sμ<δ Laμ and M¬δa = Nμ<δ M¬μa. For the inductive hypothesis for all μ < δ a ∈ OpTrueIwFσPwσ ↑(α−1) ↑ μ → wσ ∈ La μ ¬a ∈ OpFalseIwFσPwσ ↑(α−1) ↓ μ → wσ ∈ M¬μa If a ∈ OpTrueIwFσPwσ ↑(α−1) ↑ δ, then there exists a μ < δ such that a ∈ OpTrueIwFσPwσ ↑(α−1) ↑ μ. For the inductive hypothesis, wσ ∈ Lδa.
If ¬a ∈ OpFalseIwFσPwσ ↑(α−1) ↓ δ, then, for all μ < δ, ¬a ∈ OpFalseIwFσPwσ ↑(α−1) ↓ μ. For the inductive hypothesis, wσ ∈ Maδ.
Consider a limit α. Then Kaα = Sβ<α Kaβ and K¬αa = Sβ<α K¬βa. The inductive hypothesis is
a ∈ IFP wσ ↑ β → wσ ∈ Kaβ ¬a ∈ IFP wσ ↑ β → wσ ∈ K¬βa If a ∈ IFP wσ ↑ α, then there exists a β < α such that a ∈ IFP wσ ↑ β. For the inductive hypothesis wσ ∈ Kaβ so wσ ∈ Kaα. Similarly for ¬a. ♦ Theorem 7 For a ground probabilistic logic program P with atoms BP , let Kaα and Kα
¬a be the formulas associated with atom a in IFPC P ↑ α. For every atom a and total choice σ, there is an iteration α0 such that for all α > α0 we have: Theorem 8 For a ground probabilistic logic program P, let Kaα and K¬αa be the formulas associated with atom a in IFPC P ↑ α. For every atom a and every iteration α, Kaα and K¬αa are countable sets of countable composite choices.
Proof: It can be proved by observing that each iteration of OpT rueCIPFPC P ↑β and OpFalseC IPFPC P ↑β generates countable sets of countable explanations since the set of rules is countable.