Rezoluce (logika)

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

Pro výrokovou logiku má tvar

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

V predikátové logice má rezoluce podobu

${\displaystyle \displaystyle {\frac {(p\lor A)\land (\neg q\lor B)}{(A\lor B)\sigma }}}$, kde ${\displaystyle \sigma }$ je substituce unifikující ${\displaystyle p}$ a ${\displaystyle 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 A a B 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í ${\displaystyle C_{1}\land C_{2}\rightarrow R}$, a proto pokud je resolventa nesplnitelná, je nesplnitelná i původní konjunkce klauzulí. Rezoluce tedy dokazuje tvrzení sporem. Chceme-li dokázat ${\displaystyle p}$, přidáme do množiny formulí ${\displaystyle \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.