Rezoluce (logika): Porovnání verzí
Smazaný obsah Přidaný obsah
m oprava |
m formát zápisu šablon; kosmetické úpravy |
||
Řádek 1:
'''Rezoluce''' je v logice metoda automatického dokazování tvrzení zavedená Alanem Robinsonem v roce 1965.
Pro [[výroková logika|výrokovou logiku]] má tvar
Řádek 5:
V [[predikátová logika|predikátové logice]] má rezoluce podobu
:<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>. 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í]]
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í.
Řádek 14:
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ý používá [[SLI rezoluce|SLD rezoluci]] a [[Hornova klauzule|Hornovy klauzule]].
[[Kategorie:Matematická logika]]
| |||