Rezoluce (logika): Porovnání verzí

Smazaný obsah Přidaný obsah
++
reyoluce a klauyulu
Řádek 6:
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í]] odvozovací pravidlo a může být použito pro libovolné formule {{math|A}} a {{math|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í <math>C_1 \land C_2 \rightarrow R</math>, a proto pokud je resolventa nesplnitelná, je nesplnitelná i původní konjunkce klauzulí.