![Logo Matematická biologie](images/logo-matbiol.png)
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í
.
- Přejmenujeme proměnné formule
tak, aby každý vstup kvantifikátoru vázal jinou proměnnou. (Tj. např. formuli
nahradíme formulí
.)
- Spojky
,
nahradíme spojkami
a
na základě známých tautologických rovností
nahradíme
nahradíme
- 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
- 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).
- 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í.
- 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 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