the probabilistic facts in the ProbLog program, each literal’s random variable appears at most once in the conjunction representing a proof, even if the corresponding subgoal is called multiple times when constructing the proof. We therefore know that the literals in the prefix $p$ cannot be in any suffix $s_i$, hence, given ProbLog’s independence assumption, $P(p \land ( s_1\lor\ldots\lor s_n)|T) = P(p|T)P(s_1\lor\ldots\lor s_n|T) \leq P(p|T)$. Therefore, $P(d_2)$ monotonically decreases.

As an illustration, consider a probability threshold $\gamma =0\ldotp9$ for the SLD-tree in Figure \[fig:SLD\]. In this case, $d_1$ encodes the left success path while $d_2$ additionally encodes the path up to *path$(e,d)$*, i.e., $d_1 = cd$ and $d_2 = cd \vee ce$, whereas the formula for the full SLD-tree is $d = cd \vee (ce \wedge ed)$. The lower bound thus is $0\ldotp9$, the upper bound (obtained by disjoining $d_2$ to $cd \vee (ce\wedge\neg cd)$) is $0\ldotp98$, whereas the true probability is $0\ldotp94$.

Notice that in order to implement this algorithm we need to compute the probability of a set of proofs. This task will be described in detail in Section \[sec:implementation\].

### K-Best

Using a fixed number of proofs to approximate the probability allows better control of the overall 