You are here: start » vsb » ml » cviceni_2010_2011 » 7
[[vsb:ml:cviceni_2010_2011:7]]

Home Blog Programování I VŠB: ML Odkazy O mně

Table of Contents

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

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

Cvičení

  • Na tomto cvičení budeme dělat pouze příklady na skolemizaci, tzn. první příklad.
vsb/ml/cviceni_2010_2011/7.txt · Last modified: 06.03.2014 11:00 (external edit)
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki