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

===== Organizační =====

  * V první části si projdeme první zápočtovou písemku.
  * Ve druhé části představím rezoluční metodu pro PL1 a skolemizaci.

===== Teorie =====

  * Pro použití rezoluční metody na úsudky v PL1 je třeba nejdříve úsudek převést do Skolemovy klauzulární formy, což je konjunktivní normální forma.
  * Důkaz rezoluční metodou se tedy provádí sporem. Úsudek P1, P2, ..., Pn |= Z se převádí na formuli ve tvaru P1 ∧ P2 ∧ ... ∧ Pn ∧ ¬Z.

==== Postup skolemizace ====

  - Utvoření existenčního uzávěru (zachovává splnitelnost)
  - Eliminace nadbytečných kvantifikátorů
  - Eliminace spojek ⊃, ≡
  - Přesun negace dovnitř
  - Přejmenování proměnných
  - Přesun kvantifikátorů doprava
  - Eliminace existenčních kvantifikátorů (Skolemizace – zachovává splnitelnost)
  - Přesun všeobecných kvantifikátorů doleva
  - Použití distributivních zákonů

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

  * Na tomto cvičení budeme dělat pouze příklady na skolemizaci, tzn. **první** příklad.