Rezoluce (logika)

Z Wikipedie, otevřené encyklopedie
Skočit na: Navigace, Hledání

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

Pro výrokovou logiku má tvar

, kde a jsou disjunkce literálů. se nazývá resolventou.

V predikátové logice má rezoluce podobu

, kde je substituce unifikující a . 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í , a proto pokud je resolventa nesplnitelná, je nesplnitelná i původní konjunkce klauzulí. Rezoluce tedy dokazuje tvrzení sporem. Chceme-li dokázat , přidáme do množiny formulí . 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á SLI rezoluci a Hornovy klauzule.