listed below. For a predicate p, we introduce iff(p), the iff definition of p by

$\mathrm{iff}\,(p)\ \ \stackrel{{\mathrm{def}}}{{=}}\ \ \forall\,x\ \left(p(x\,)\leftrightarrow\,\exists\,y_{1}(x\,=t_{1}\wedge W_{1}\,)\vee\cdots\vee\,\exists\,y_{n}(\,x\,=t_{n}\wedge W_{n}\,)\,\right).$
Here x is a vector of new variables of length equal to the arity of p, p(t,) ~ W, (1 ~ i ~
n, 0 ≤ n), an enumeration of clauses about p in DB, and y i , a vector of variables occurring in p(ti) { Wi. Then define comp(R) as follows.

{B | B is a ground instance of a clause head appearing in R} head( R ) d ef iff ( R ) {iff(p) | p appears in a clause head in R} d ef Eq {f(x) = f(y) → x = y | f is a function symbol} ∪ { f ( x ) ̸ = g ( y ) | f and g are different function symbols} ∪ {t ̸ = x | t is a term properly containing x } comp(R)   dcf   iff(R)  U  Eq
E q , Clark's equational theory (Clark, 1978), deductively simulates unification.  Likewise comp(R) is a first-order theory which deductively simulates SLD refutation with the help of E o by replacing a clause head atom with the clause body (Lloyd, 1984; Doets, 1994).

We here introduce some definitions which will be frequently used. Let B be an atom.

An explanation for B w.r.t. DB = F ∪ R is a conjunction S such that S, R H B, and as a set comprised of its conjuncts, S ⊂ F holds and no proper subset of S satisfies this. The set of all explanations for B is called the support set for B and designated by ψ DB ( B ). 18

## 4.1 Motivating Example

First of all, we review distribution sem antics by a concrete example. Consider the following program DB b = F b ∪ R b in Figure 1 modeling how one's blood type is determined by blood type genes probabilistically inherited from the parents. 19 The first four clauses in R b state a blood type is determined by a genotype, i.e. a pair of blood type genes a, b and o. For instance, btype('A'):- (gtype(a,a) ; gtype(a,o) ;
gtype(o,a)) says that one's blood type is A if his (her) genotype is (a,a), (a,o) or (o,a).

These are propositional rules.

Succeeding clauses state general rules in terms of logical variables. The fifth clause ssee to the seemed to th (X,Y)) is caused by two events, gene(father,X) (inheriting gene X from the father) and gene(mother,Y) (inheriting gene Y from the mother). gene(P,G):- msw(gene,P,G) is a clause connecting rules in R b with probabilistic facts in F b . It tells us that the gene G is inherited from a parent P if a choice represented by msw(gene,P,G) 20 is made. The