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

===== 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.
  * Tuto následně rozepíšeme na řádky podobně jako u výrokové logiky.
  * Abychom mohli použít rezoluční pravidlo, tak musíme provádět tzv. unifikaci, tedy náhradu proměnných za termy.

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

  * Na tomto cvičení budeme dělat zbývající příklady, tedy unifikaci a rezoluční metodu.