====== Cvičení 4.10.2010 ======

===== Teorie =====

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:

  - 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ý**.
  - 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ý**.

===== Cvičení =====

  * 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.