to decrease $P(d_2|T)-P(d_1|T)$.

Given an acceptance threshold $\delta_p$, an initial probability threshold $\gamma$, and a shrinking factor $\beta\in(0,1)$, the algorithm proceeds in an iterative-deepening manner as outlined in Algorithm \[alg:delta\]. Initially, both $d_1$ and $d_2$ are set to <span style="font-variant:small-caps;">False</span>, the neutral element with respect to disjunction, and the probability bounds are $0$ and $1$, as we have no full proofs yet, and the empty partial proof holds in any model.

$d_1 = $ <span style="font-variant:small-caps;">False</span>; $d_2 = $ <span style="font-variant:small-caps;">False</span>; $P(d_1|T) =0$; $P(d_2|T) = 1$; $p = $<span style="font-variant:small-caps;">True</span>; Expand current proof $p$ set $d_2 = $ <span style="font-variant:small-caps;">True</span> Compute $P(d_1|T)$ and $P(d_2|T)$ $\gamma := \gamma\cdot\beta$ return $[P(d_1|T),P(d_2|T)]$

It should be clear that $P(d_1|T)$ monotonically increases, as the number of proofs never decreases. On the other hand, as explained above, if $d_2$ changes from one iteration to the next, this is always because a partial proof $p$ is either removed from $d_2$ and therefore no longer contributes to the probability, or it is replaced by proofs $p_1,\ldots , p_n$, such that $p_i = p \land s_i$, hence $P(p_1 \lor \ldots \lor p_n|T) = P(p \land s_1\lor\ldots\lor p\land s_n|T) = P(p \land ( s_1\lor\ldots\lor s_n)|T)$. As proofs are subsets of 