to tackle the disjoint-sum-problem at the end of this section, we will now discuss the two steps of ProbLog’s exact inference in more detail.

![SLD-tree for query *path$(c,d)$.*[]{data-label="fig:SLD"}](sld)

Following Prolog, the first step employs SLD-resolution to obtain all different proofs. As an example, the SLD-tree for the query *?- path$(c,d)$.* is depicted in Figure \[fig:SLD\]. Each successful proof in the SLD-tree uses a set of ground probabilistic facts $\{p_1::c_1, \cdots, p_k::c_k\}
\subseteq T$. These facts are necessary for the proof, and the proof is *independent* of other probabilistic facts in $T$.

Let us now introduce a Boolean random variable $b_i$ for each ground probabilistic fact $p_i::c_i \in T$, indicating whether $c_i$ is in a sampled logic program, that is, $b_i$ has probability $p_i$ of being true.[^2] A particular proof of query $q$ involving ground facts $\{p_1::c_1, \cdots, p_k::c_k\}
\subseteq T$ is thus represented by the conjunctive formula $b_1
\wedge \cdots \wedge b_k$, which at the same time represents the set of all subprograms containing these facts. Furthermore, using $E(q)$ to denote the set of proofs or explanations of the goal $q$, the set of all subprograms containing *some* proof of $q$ can be denoted by $\bigvee_{e \in E(q) } \, 