Rezoluce (logika)

Rezoluce je v logice metoda automatického dokazování tvrzení zavedená Alanem Robinsonem v roce 1965.

Pro výrokovou logiku má tvar

$\frac{(p\vee A)\wedge (\mathrm{\neg }p\vee B)}{A\vee B}$, kde $A$ a $B$ jsou disjunkce literálů. $A\vee B$ se nazývá resolventou.

V predikátové logice má rezoluce podobu

$\frac{(p\vee A)\wedge (\mathrm{\neg }q\vee B)}{(A\vee B)\sigma }$, kde $\sigma$ je substituce unifikující $p$ a $q$. V obecnosti je možné a obecně nutné vybrat a unifikovat víc pozitivních literálů v jedné a víc negovaných literálů ve druhé klauzuli.

Rezoluce je korektní odvozovací pravidlo a může být použito pro libovolné formule Šablona:Math a Šablona:Math ve výrokové i predikátové logice. Při dokazování a problému splnitelnosti (SAT) se obecné formule převedou na klauzule a pak stačí rezoluce jako jediné odvozovací pravidlo.

Resolventa není ekvivalentní původní konjunkci klauzulí, ale platí $C_1\wedge C_2\to R$, a proto pokud je resolventa nesplnitelná, je nesplnitelná i původní konjunkce klauzulí. Rezoluce tedy dokazuje tvrzení sporem. Chceme-li dokázat $p$, přidáme do množiny formulí $\mathrm{\neg }p$. Pokud rezoluce dojde ke sporu (tj. k prázdné klauzuli, jinými slovy ke klauzuli s prázdnou množinou literálů), je uvažovaná množina formulí nesplnitelná a podle Herbrandovy věty tím je tvrzení dokázáno.

V logice s rovností se k rezoluci přidává odvozovací pravidlo paramodulace.

Na principu rezoluce jsou založeny logické programovací jazyky, například Prolog, který používá SLD rezoluci a Hornovy klauzule. Šablona:Autoritní data