Cvičení 4.10.2010

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:

1. obdržíme na dvou řádcích elementární výrok jednou přímo a jednou negovaný - kdybychom v takovém stavu formuli pak opět složili pomocí konjunkcí, tak je spor zřejmý - formule je kontradikce, původní formule je tedy tautologie a úsudek je platný.
2. přestože jsme získali všechny literály, které jsme mohli, tak jsme nenašli spor; negovaná formule tedy není kontradikce, původni formule není tautologie a úsudek není platný.

• V prvním příkladu si zopakujeme metody zjišťování platnosti úsudku z minulých cvičení a vyzkoušíme rezoluční metodu.
• V druhém příkladu zkusíme místo ověřování zadaného úsudku vytvořit úsudky vlastní. Třetí příklad je velmi podobný, ovšem zde je zadání již formalizováno.
• Čtvrtý příklad je zaměřen na pochopení pricipu rezoluční metody a na procvičení dobré orientace v zápisu po řádcích.