Automatické dokazování v predikátové logice (obecná rezoluční metoda)

Jak jsme uvedli v předchozí kapitole, sémantický důkaz logické pravdivosti a tedy i logického vyplývání zkoumáním všech možných interpretací je v predikátové logice často obtížný. Jednou z efektivních metod je však rezoluční metoda, která je pro predikátovou logiku zobecněním základní rezoluční metody výrokové logiky. Oproti výrokové logice se nám zde objeví dvě komplikace, které jsou kvantifikátory a objektové proměnné.

V predikátové logice nemůžeme díky kvantifikátorůmm provést okamžitý převod formule do klauzulárního tvaru, o který se rezoluční metoda opírala v případě výrokového počtu. Řešení je takové, že se obecných kvantifikátorů zbavíme tak, že budeme předpokládat, že všechny volné proměnné ve formulích jsou obecně kvantifikovány. Existenčních kvantifikátorů se zbavíme tzv. skolemizací. Výsledný tvar klauzule se pak nazývá Skolemova klauzulární forma.

Rezoluční metodu lze aplikovat právě pouze na formule, které jsou v Skolemově klauzulární  formě. Obecně pak postup vypadá tak, že chceme-li zjistit, zda , aplikujeme rezoluční metodu na formuli , neboť pokud je tato formule nesplnitelná, pak je formule tautologie a vztah platí.

Definice: Literál je atomická formule (tzv. pozitivní literál), nebo negace atomické formule (tzv. negativní literál), například  jsou literály.

Definice: Klausule je taková sentence, že všechny kvantifikátory jsou obecné a stojí na začátku sentence (na jejich pořadí nezáleží) a za nimi následují literál, nebo disjunkce literálů. Tedy např. ,  jsou klausule, ale  nejsou klausule.

Definice: Skolemova klauzulární forma – je uzavřená formule, která je formátu  a kde  jsou klausule. Všechny kvantifikátory zde stojí na začátku formule a formule neobsahuje žádný existenční kvantifikátor.