Řešení LP rezoluční metodou

• EDB jako množina tvrzení

• IDB jako množina Hornových klauzulí:

• F(x,y)  M(x)

• F(x,y)  F(x,w) S(y,w)

• S(x,y)  M(x)  B(x,y)

• Předpoklad: formule v IDB jsou univerzálně kvantifikované, např.:

• xyw ( F(x,y) F(x,w) S(y,w) )

• Reformulace D1 z B(z,Pavel)