Weakest Preimage

The weakest preimage of a conclusion C with respect to a proof P is the most general set of assertions A, such that A entails C according to P.
Prolog-EGB computes the most general rule that can be justified by the explanation by computing the weakest preimage.
It is calculated by using regression—work iteratively backward through the explanation, computing the weakest preimage at each step.
   SafeToStack(x, y)
4. Lighter(o1, o2) → SafeToStack(o1,o2)
   Lighter(x, y)
3. Weight(o1, 0.6) ∧ LessThan(0.6, 5) ∧ Weight(o2,5) → Lighter(o1,o2)
  Weight(x,wx), LessThan(wx, wy), Weight(y,wy)
2. Type(o2,endtable) → Weight(o2,5)
   Weight(x,wx), LessThan(wx,5), Type(y,endtable)
1. Volume(o1,2) ∧ Density(o1,0.3) ∧ Equal(0.6, 2*0.3) → Weight(o1,0.6)
   Volume(x,vx), Density(x,dx), Equal(wx, vx*dx), LessThan(wx,5), Type(y,endtable)
The final Horn clause has a body that corresponds to the weakest preconditions, and the head is the concept:
SafeToStack(x,y) ← Volume(x, vx) ∧ Density(x,dx) ∧ Equal(wx, vx*dx) ∧ LessThan(wx,5) ∧ Type(y,endtable)