such a program has to contain, i.e., all the ground probabilistic facts used in that proof. As probabilistic facts correspond to random variables indicating the presence of facts in a sampled program, we alternatively denote proofs by conjunctions of such random variables. In our example, query *path(c,d)* has two proofs in the full program: *{edge(c,d)}* and *{edge(c,e),edge(e,d)}*, or, using logical notation, $cd$ and $ce \wedge ed$. The set of all subprograms containing *some* proof thus can be described by a disjunction over all possible proofs, in our case, $cd \vee (ce \wedge ed)$. This idea forms the basis for the inference method presented in [@DeRaedt07], which uses two steps:

1.  Compute the proofs of the query $q$ in the logical part of the theory $T$, that is, in $BK \cup L_T$. The result will be a DNF formula.

2.  Compute the probability of this formula.

Similar approaches are used for PRISM [@SatoKameya:01], ICL [@Poole00] and pD [@Fuhr00].

The probability of a single given proof, cf. Equation (\[eq:deriv\_px\]), is the marginal over all programs allowing for that proof, and thus equals the product of the probabilities of the facts used by that proof. However, we cannot directly sum the results for 