\ldots\wedge b_n$ will always be at most the probability of an arbitrary prefix $b_1 \wedge \ldots\wedge b_i, i\leq n$. In our example, the probability of the second proof will be at most the probability of its first edge from $c$ to $e$, i.e., $P(ce|T) = 0\ldotp8 \geq 0\ldotp4$. As disjoining sets of proofs, i.e., including information on facts that are *not* elements of the subprograms described by a certain proof, can only decrease the contribution of single proofs, this upper bound carries over to a set of proofs or partial proofs, as long as prefixes for all possible proofs are included. Such sets can be obtained from an incomplete SLD-tree, i.e., an SLD-tree where branches are only extended up to a certain point.

This motivates ProbLog’s *bounded approximation algorithm*. The algorithm relies on a probability threshold $\gamma$ to stop growing the SLD-tree and thus obtain DNF formulae for the two bounds[^3]. The lower bound formula $d_1$ represents all proofs with a probability above the current threshold. The upper bound formula $d_2$ additionally includes all derivations that have been stopped due to reaching the threshold, as these still *may* succeed. Our goal is therefore to grow $d_1$ and $d_2$ in order 