entails some ground instance of $q$, and vice versa, each subprogram entailing $q$ is an extension of some explanation of $q$. As the DNF now contains conjunctions representing fully specified programs, its probability is a sum of products, which directly corresponds to Equation (\[eq:p\_suc\]): $$\begin{aligned}
\lefteqn{ P(\bigvee_{ L \subseteq L_T, \exists\theta L\union BK \models q\theta }  \left( \bigwedge_{c_i \in  L } b_i  \wedge \bigwedge_{c_i \in L_T \backslash L} \neg b_i\right)) }\\
&=& \sum_{ L \subseteq L_T, \exists\theta L\union BK \models q\theta }  \left( \prod_{c_i \in  L } p_i  \cdot \prod_{c_i \in L_T \backslash L} (1- p_i)\right)\\
&=& \sum_{ L \subseteq L_T, \exists\theta L\union BK \models q\theta }  P(L|T)\end{aligned}$$ We thus obtain the following alternative characterisation of the success probability: $$P_s(q|T) = P\left( \bigvee_{e \in E(q) } \, \bigwedge_{c_i \in e} b_i \right)
  \label{eq:dnf}$$ where $E(q)$ denotes the set of proofs or explanations of the goal $q$ and $b_i$ denotes the Boolean variable corresponding to ground probabilistic fact $p_i::c_i$. Thus, the problem of computing the success probability of a ProbLog query can be reduced to that of computing the probability of a DNF formula.

However, as argued above, due to overlap between different conjunctions, the proof-based DNF of Equation (\[eq:dnf\]) cannot 