Matematické Fórum

radekskrabal · 31. 12. 2011 01:30

Je dána teorie $T = \{\forall x (\neg P(x) \Rightarrow Q(x)), \forall x \neg Q(f(x)), \forall z (P(f(z)) \Rightarrow \neg R(z)) \}$ a formule $\varphi = \forall y \neg R(y)$ . Zjistěte, zda platí $T \vdash \varphi$ .

Převod na klauzární tvar:
$K_1: P(x) \vee Q(x)$
$K_2: \neg Q(f(x))$
$K_3: \neg P(f(z)) \vee \neg R(z)$
$K_4: R(y)$

Rezoluční metoda odvozování:

1. krok - přejmenování proměnné x na t v K1, substituce f(x) za t
2. krok - přejmenování proměnné z na x v K3
3. krok - přejmenování proměnné y na x v K4

Může mi prosím někdo napsat názor na to, zda je takové odvození korektní, případně kde jsem udělal chybu?

Předem díky za reakce!

Matematické Fórum

#1 31. 12. 2011 01:30

Sémantický důsledek rezoluční metodou (predikátová logika)

Zápatí