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\frac{(p \lor A) \land (\neg p \lor B)}{A \lor B}, kde A a B jsou disjunkce literálů. A \lor B se nazývá resolventou.

V predikátové logice má rezoluce podobu :\displaystyle\frac{(p \lor A) \land (\neg q \lor B)}{(A \lor 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 a 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 \land C_2 \rightarrow R, a proto pokud je resolventa nesplnitelná, je nesplnitelná i původní konjunkce klauzulí. Rezoluce tedy dokazuje tvrzení sporem. +more Chceme-li dokázat p, přidáme do množiny formulí \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.

Kategorie:Matematická logika