Matematické Fórum

Zdravím,
mám dotaz ohledně rezoluční metody ve výrokové logice. Zkoušel jsem si počítat tento příklad:



Jde mi o to, že ač ve výsledcích je napsáno, že není důsledkem, tak mě vyšlo, že ano a chci se zeptat, kde dělám chybu. Další věc je, že jsem zkusil trošku jiný postup a už to vyšlo správně. Myslel jsem, že můžu volit libovolné proměnné a sestavovat rezolventy z libovolných klauzulí, teda tak to píše ve svých skriptech paní Demlová a výsledek by měl být stejný. Zkusím popsat postup příkladů:

První tabulka:
  1. Udělám rezolventy podle R, obě jsou tautologie, takže žádný sloupec nepřipíšu.
  2. Poté udělám rezolventy podle Q
  3. Zvolím proměnnou S a podle ní udělám rezolventy. Jedna je tautologie a druhá je negace P
  4. Poslední zbývá P a pokud udělám rezolventu, zůstane prázdná klauzule, tudíž je množina nesplnitelná, takže jde o důsledek.

Druhá tabulka.
  První dva kroky stejné.
  3. Zvolím proměnnou P a podle ní udělám rezolventy. Jedna je tautologie, druhá negace S
  4. Poslední zbývá S, zde nelze udělat rezolventu, takže jen zapíši a množina je splnitelná, takže nejde o důsledek




Mohl by mi někdo poradit, kde dělám chybu? Jsou nějaká pravidla, jak volit pořadí proměnných a tvorbu jejich rezolvent?

Myslel jsem, že rezolučku zvládám dobře, ale tohle mě zaskočilo a navíc jsem narazil ještě na jeden příklad.

Děkuji mockrát za pomoc.