Rezoluce (logika): Porovnání verzí
Smazaný obsah Přidaný obsah
reyoluce a klauyulu |
m -link SAT |
||
Řá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>. 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
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í.
|