Toto cvičení se zaměří na rezoluční metodu ve výrokové logice. Podrobnější vysvětlení teoretického podkladu bude na přednašce, ve cvičení projdeme především praktické informace o této metodě.
Rezoluční metoda se používá především při důkazu sporem. Úsudek tedy klasicky nejdříve převedeme na formu tautologie a výslednou formuli znegujeme. Tím získáme formuli, kterou lze snadno převést na konjuntivní normální formu převedením všech operátorů na disjunkce, konjunkce a negace.
Vzhledem k tomu, že se jedná o důkaz sporem, dokazujeme nyní, že negovaná formule je kontradikce. K tomu využíváme tzv. rezoluční pravidlo:
|= (A || B) && (!A || C) ⇒ (B || C)
Všimněte si, že se nejedná o ekvivalentní úpravu. Pro potřeby důkazu sporem je ovšem tato implikace postačující. Toto pravidlo lze také chápat jako schéma, ve kterém B a C mohou zastupovat jakoukoliv disjunkci literálů.
Pro zjednodušení důkazu si negovanou formuli rozdělíme podle konjunkcí na řadky - na každém řádku tedy budeme mít buď samostatný literál nebo elementární disjunkci. Postup důkazu se pak skládá z jednotlivých kroků, ve kterých hledáme vždy na dvou samostatných řádcích části formule podle schématu rezolučního pravidla (tedy takové řádky, kde se výrok jednou vyskytuje přímo a jednou negovaně).
Tím získáváme jednodušší a jednodušší elementární disjunkce, které lze z negované formule odvodit. Důkaz může skočit dvěma způsoby: