Slovník | Vyhledávání | Mapa webu
 
Základy informatiky pro biologyTeoretické základy informatiky Predikátová logika Automatické dokazování v predikátové logice (obecná rezoluční metoda) Postup převodu sentence do klausálního tvaru

Logo Matematická biologie

Postup převodu sentence do klausálního tvaru

Nejprve vyřešíme, jak pro danou množinu formulí najít množinu klausulí takovou, že množina je splnitelná právě tehdy, když je splnitelná množina . Nepožadujeme, aby množiny a byly tautologicky ekvivalentní, to by totiž obecně nebylo možné. Jedná se tak o obdobu konjunktivní normální formy pro danou formuli ve výrokové logice. Toto nám následně pomůže využít rezoluční metodu pro zjištění, zda daná množina sentencí je splnitelná i zda daná sentence sémanticky vyplývá z dané množiny sentencí. Následující kroky převedou danou sentenci do množiny klausulí .

  1. Přejmenujeme proměnné formule tak, aby každý vstup kvantifikátoru vázal jinou proměnnou. (Tj. např. formuli  nahradíme formulí .)
  2. Spojky , nahradíme spojkami a na základě známých tautologických rovností
    • nahradíme
    • nahradíme
  3. Přesuneme spojku „co nejníže v derivačním stromu formule, tj. až před atomické formule. Použijeme k tomu vztahy
    • nahradíme
    •  nahradíme
    • nahradíme
    •  nahradíme
    • nahradíme
  4. Přesuneme spojku „co nejníže v derivačním stromu formule pomocí vztahů
    • nahradíme
    • nahradíme
    • nahradíme

Přitom dáváme přednost první rovnosti. Teprve v případě, že první rovnost nelze aplikovat, používáme další dvě rovnosti. Uvědomte si, že druhá rovnost je opravdu tautologická ekvivalence pouze proto, že formule α neobsahuje proměnnou (viz krok 1).

  1. Použijeme tautologickou ekvivalenci a nahradíme  k distribuci obecného kvantifikátoru. Jestliže nyní formule neobsahuje existenční kvantifikátor, máme formuli , která je konjunkcí klausulí. Tuto formuli tedy nahradíme množinou jejích klausulí.
     
  2. Obsahuje-li formule existenční kvantifikátor, nahradíme každou uzavřenou podformuli tvaru  formulí , kde je libovolný nový funkční symbol arity . Je-li , použijeme nový konstantní symbol .

 

Úloha: Převeďme na klausální tvar následující formuli  (jinými slovy, najděte množinu klausulí , která je splnitelná právě tehdy, když je splnitelná sentence ).

 

Řešení:

Krok 1.
Přejmenujeme proměnnou na v podformuli , dostaneme pak .

Krok 2.

Nahradíme spojku : .

Krok 3.

Přesuneme spojku až před atomické formule:

Krok 4 a 5 není potřeba.

Krok 6.

Protože sentence obsahuje existenční kvantifikátory, provedeme skolemizaci. Postupně odstraňujeme existenční kvantifikátory a to v pořadí, v jakém se objevují v derivačním stromu.
, zavedli jsme nový konstantní symbol a místo proměnné x a dosadili ho za všechny výskyty proměnné .
. Zavedli jsme nové konstantní symboly , ; místo proměnné , místo proměnné . Dostali jsme formuli, která je konjunkcí dvou klausulí, proto

 

 
vytvořil Institut biostatistiky a analýz Masarykovy univerzity | | zpětné odkazy | validní XHTML 1.0 Strict