Řešení LP rezoluční metodou

• Tv.: Rezolventa je (ne)splnitelná, byly-li vstupní klauzule (ne)splnitelné

• Cíl procedury: odvodit NIL

• Zdůvodnění:

• W=A1,...,Am, pak W A právě když

• A1AmA je nesplnitelná

• Podle Gödelovy věty je nesplnitelnost částečně rozhodnutelná, tj. existuje procedura P tak, že pro každou formuli  platí:

• je-li nesplnitelná, P() se zastaví a oznámí to,

• je-lisplnitelná, P() buď skončí a oznámí to, nebo neskončí.