Verze z 21. 12. 2013, 15:08 editovat Jj14 (diskuse \| příspěvky) Prověření uživatelé 88 592 editací m tzpo ← Přejít na předchozí porovnání		Verze z 21. 12. 2013, 15:32 editovat zrušit editaci Jj14 (diskuse \| příspěvky) Prověření uživatelé 88 592 editací fixx Přejít na další porovnání →
Řádek 8: Resolventa 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ě~~klauzuli, ~~formulí~~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 (programovací jazyk)\|Prolog]], který využívá [[Hornova klauzule\|Hornovy klauzule]]. [[Kategorie:Matematická logika]]

Rezoluce (logika): Porovnání verzí