Rezoluční princip

V predikátové logice je logické odvozování, spolu s výsledkem o korektnosti a úplnosti, jedinou cestou, jak zjišťovat splnitelnost množiny formulí. Zde nelze použít tabulkovou metodu oblíbenou ve výrokové logice pro svoji exponenciální časovou náročnost vzhledem k počtu proměnných. Množina všech možných interpretací predikátových formulí je totiž potenciálně nekonečná. Jednou z možností, jak odvozování alespoň částečně automatizovat, je resoluční princip.

Jeho princip je takový, že prvně všechny formule převedeme do tautologicky ekvivalentních formulí v konjunktivní normální formě (klausule). Pokud lze v některé dvojici klausulí nalést komplementární literály (dvojici literálů, kde jeden je negací druhého), vytvoříme jejich resolventu, tj. novou klausuli, kde vynecháme komplementární literály. Tento postup opakujeme tak dlouho, dokud lze najít dvojici klausulí s komplementárními literály nebo pokud nezískáme prázdnou klasuli (resolventu). Pokud proces končí získáním prázdné klausule, je daná množina klausulí nesplnitelná. Pokud se proces vytváření zastaví bez získání prázdné klausule, množina klasulí je splnitelná.

V predikátové logice je idea resolučního principu totožná s postupem ve výrokové logice. Komplementarita literálů pro úspěšnou tvorbu resolventy dvou klausulí bude v predikátové logice ale podmíněna hledáním speciální substituce (maximálního unifikátoru). Postup hledání vhodné substituce se označuje jako unifikační algoritmus.

Chceme-li tedy rozhodnout, zda je splnitelná množina klausulí S, sestrojíme množinu , tak, že k přidáme resolventy prvého řádu. Dále přidáme resolventy , získáme a pokračujeme, dokud nenastane rovnost . Dostaneme tak množiny:

Resoluční princip predikátové logiky říká, že množina je splnitelná právě když  neobsahuje prázdnou klausuli.