Rezoluce (logika): Porovnání verzí
Smazaný obsah Přidaný obsah
Bez shrnutí editace |
Bez shrnutí editace |
||
Řádek 7:
:<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í]] <math>p</math> a <math>q</math>.
Resoventa není ekvivalentní původní konjunkci klauzulí, ale platí <math>C_1 \land C_2 \rightarrow R</math>, a proto pokud je resolventa nesplnitelná, je nesplnitelná i původní konjunkce klauzulí.
Rezoluce tedy dokazuje tvrzení [[důkaz sporem|sporem]]. Chceme-li dokázat <math>p</math>, přidáme do množiny formulí <math>\neg p</math>. Pokud rezoluce dojde ke sporu (tj. k prázdné množině formulí), 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]].
| |||