Table of Contents

Cvičení 8.11.2010

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.