  Many representation schemes combining first-order logic and probability have
been proposed in recent years. Progress in unifying logical and probabilistic
inference has been slower. Existing methods are mainly variants of lifted
variable elimination and belief propagation, neither of which take logical
structure into account. We propose the first method that has the full power of
both graphical model inference and first-order theorem proving (in finite
domains with Herbrand interpretations). We first define probabilistic theorem
proving, their generalization, as the problem of computing the probability of a
logical formula given the probabilities or weights of a set of formulas. We
then show how this can be reduced to the problem of lifted weighted model
counting, and develop an efficient algorithm for the latter. We prove the
correctness of this algorithm, investigate its properties, and show how it
generalizes previous approaches. Experiments show that it greatly outperforms
lifted variable elimination when logical structure is present. Finally, we
propose an algorithm for approximate probabilistic theorem proving, and show
that it can greatly outperform lifted belief propagation.
