Rezoluce (logika): Porovnání verzí

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

Pro výrokovou logiku má tvar

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

:<math>\displaystyle\frac{(p \lor A) \land (\neg q \lor B)}{(A \lor B)\sigma}</math>, kde <math>\sigma</math> je substituce [[Unifikace (logika)|unifikující]] ''p'' a ''q''.

Rezoluce [[důkaz sporem|dokazuje tvrzení sporem]]. Chceme-li dokázat ''p'', přidáme do množiny formulí <math>\neg p</math>. Pokud rezoluce dojde ke sporu (tj. k prázdné množině formulí), je tvrzení dokázáno.