3.3. Rezoluční metoda v predikátové logice [080204-1424] 19
3.3 Rezoluční metoda v predikátové logice
3.3.1 Příklad. Pro každé dva následující literály rozhodněte, zda existuje
substituce, po níž se stanou stejnými literály. V kladném případě najděte
nejobecnější takovou substituci.
a) P(x, y), P(t, f(z));
b) Q(a, y, f(y)), Q(z, z, u);
c) R(x, g(x)), R(y, y);
d) F(a, x), F(y, b);
e) Q(x, f(y), z), Q(g(w), u, g(w));
f) P(g(x), y), P(u, f(w)).
Výsledek: a) Po substituci θ = {x/t, y/f(z)} z obou literálů vznikne literál
P(t, f(z)).
b) Po substituci θ = {z/a, y/a, u/f(a)} z obou literálů vznikne literál
Q(a, a, f(a)).
c) Taková substituce neexistuje.
d) Po substituci θ = {y/a, x/b} z obou literálů vznikne literál F(a, b).
e) Po substituci θ = {x/g(w), u/f(y), z/g(w)} z obou literálů vznikne literál
Q(g(w), f(y), g(w)).
f) Po substituci θ = {u/g(x), y/f(w)} z obou literálů vznikne literál
P(g(x), f(w)).
3.3.2 Příklad. Najděte všechny rezolventy následujících klausulí.
a) P(x, y) ∨ Q(y, z), ¬P(u, f(u));
b) P(x, x) ∨ ¬Q(x, f(x)), Q(x, y) ∨ R(y, z);
c) P(x, y) ∨ ¬Q(y, x), Q(x, x) ∨ P(y, f(x));
d) P(x, y) ∨ ¬S(x, x) ∨ T(x, f(x), z), ¬T(f(x), x, z) ∨ S(x, z);
e) ¬Q(x, y, z) ∨ ¬Q(y, y, y), Q(x, f(x), z) ∨ Q(z, t, t).
Výsledek: a) Q(f(u), z);
b) P(x, x) ∨ R(f(x), z);
c) P(x, x) ∨ P(z, f(x)), uvědomte si, že jsme nejprve přejmenovali proměnné
tak, že naše klauzule jsou P(x, y) ∨ ¬Q(y, x) a Q(t, t) ∨ P(z, f(t)), pak hledaná
substituce je θ = {y/x, t/x} ;
d) P(x, y)∨T(x, f(x), z)∨¬T(f(x), x, x) (z literálů T(x, f(x), z) a ¬T(f(x), x, x)
žádnou substitucí nevzniknou komplementární literály). Zase si je dobré uvědomit,
že nejprve musíme přejmenovat proměnné tak, abychom v obou klauzulích
měli různá jména proměnných;
e) ¬Q(f(x), f(x), f(x))∨Q(z, t, t), ¬Q(y, y, y)∨Q(t, f(t), v), ¬Q(x, y, z)∨Q(t, f(t), y).
Marie Demlová: Příklady k předmětu Matem. logika 4. února 2008, 14:24
20 [080204-1424]
3.3.3 Příklad. Následující formule převeďte na klausální tvar.
a) ∀x [∃y (Q(x, y) ∨ ¬P(x, y)) ∧ ∃y (¬Q(y, x) ∨ P(y, x))];
b) ∀x [(∃y (P(x, y) ∧ ¬Q(y, x))) ∨ ∀y ∃z R(x, y, z)];
c) ¬∀x [∃y Q(x, y) ⇒ ∀y ∃z ¬P(x, y, z)];
d) ∃x S(x) ⇒ [∀x (P(x) ∨ Q(x)) ⇒ ∀x ∃y T(x, y)].
Výsledek: a) Formule je splnitelná právě tehdy, když je splnitelná formule:
[∀x (Q(x, f(x)) ∨ ¬P(x, f(x)))] ∧ [∀x (¬Q(g(x), x) ∨ P(g(x), x))] a to je právě
tehdy, když je splnitelná tato množina klausulí:
{Q(x, f(x)) ∨ ¬P(x, f(x)), ¬Q(g(x), x) ∨ P(g(x), x)}. Zde f a g jsou unární
skolemizační funkční symboly.
b) Formule je splnitelná právě tehdy, když je splnitelná formule:
∀x ∀t [(P(x, f(x)) ∨ R(x, t, g(x, t))) ∧ (¬Q(f(x), x) ∨ R(x, t, g(x, t)))]
a to je právě tehdy, když je splnitelná tato množina klausulí:
{P(x, f(x)) ∨ R(x, t, g(x, t)), ¬Q(f(x), x) ∨ R(x, t, g(x, t))}.
Zde f je unární a g je binární skolemizační funkční symbol. Tento výsledek
odpovídá převedení na formuli:
∀x ∃y ∀t ∃z [(P(x, y) ∨ R(x, t, z)) ∧ (¬Q(y, x) ∨ R(x, t, z))].
Kdybychom volili jiné pořadí úprav podle kroku 4., mohli jsme též dostat
formuli:
∀x ∀t ∃z ∃y [(P(x, y) ∨ R(x, t, z)) ∧ (¬Q(y, x) ∨ R(x, t, z))],
které by odpovídala tato množina klausulí:
{P(x, f(x, t)) ∨ R(x, t, g(x, t)), ¬Q(f(x, t), x) ∨ R(x, t, g(x, t))}.
Zde oba skolemizační funkční symboly jsou binární.
c) Formule je splnitelná právě tehdy, když je splnitelná formule:
Q(a, b) ∧ ∀z P(a, c, z)
a to je právě tehdy, když je splnitelná tato množina klausulí:
{Q(a, b), P(a, c, z)}.
Zde a, b a c jsou skolemizační konstantní symboly.
d) I zde je možných několik výsledků. Vybereme ten, kde skolemizační
funkční symboly jsou nejméně ární, tj. závisí na nejmenším počtu argumentů:
Formule je splnitelná právě tehdy, když je splnitelná formule:
∃y ∀z ∃t ∀x [(¬S(x)∨T(z, t)∨¬P(y))∧(¬S(x)∨T(z, t)∨¬Q(y))] a také formule:
∀z ∀x [(¬S(x) ∨ T(z, f(z)) ∨ ¬P(a)) ∧ (¬S(x) ∨ T(z, f(z)) ∨ ¬Q(a))]
a to je právě tehdy, když je splnitelná tato množina klausulí:
{¬S(x) ∨ T(z, f(z)) ∨ ¬P(a), ¬S(x) ∨ T(z, f(z)) ∨ ¬Q(a)}.
Zde f je unární skolemizační funkční symbol a a je skolemizační konstanta.
3.3.4 Příklad. Rezoluční metodou rozhodněte, zda platí:
a) ∀x (P(x) ∨ Q(x))
∃x ¬P(x)
∃x Q(x)
b) ∃x ∀y P(x, y)
∀x ∀y (¬P(x, y) ∨ Q(x, y))
∃x ∀y Q(x, y)
Marie Demlová: Příklady k předmětu Matem. logika 4. února 2008, 14:24
3.3. Rezoluční metoda v predikátové logice [080204-1424] 21
c) (∃x P(x)) ⇒ Q(a)
∀x (P(x) ⇒ Q(a))
Výsledek: a) Úsudek je správný: Množina klausulí S = {P(x)∨Q(x), ¬P(a), ¬Q(y)}
je nesplnitelná, neboť F ∈ R2
(S).
b) Úsudek je správný: Množina klausulí S = {P(a, y), ¬P(x, z)∨Q(x, z), ¬Q(t, f(t))}
je nesplnitelná, neboť F ∈ R2
(S).
c) Úsudek je správný: Množina klausulí S = {¬P(x) ∨ Q(a), P(b), ¬Q(a)} je
nesplnitelná, neboť F ∈ R2
(S).
3.3.5 Příklad. Rezoluční metodou ověřte správnost úsudku:
P(b) ⇒ V (a)
(∀x V (x)) ∨ (∀x ¬V (x))
P(b)
∀x V (x)
kde P je unární predikátový symbol, V je unární predikátový symbol a a, b
jsou konstantní symboly.
Výsledek: a) Úsudek je správný: Množina klausulí S = {¬P(b)∨V (a), V (x)∨
∨ ¬V (y), P(b), ¬V (b)} je nesplnitelná, neboť F ∈ R3
(S).
3.3.6 Příklad. Následující úsudek zformalizujte a rezoluční metodou rozhodněte,
zda je správný.
a) Žádný žák této třídy není hudebník.
Všichni hudebníci jsou umělci.
Žádný žák této třídy není umělec.
b) Žádný atlet nemá špatnou fyzickou kondici.
Někteří přítomní jsou atleti.
Někteří přítomní nemají špatnou fyzickou kondici.
c) Žádný atlet nemá špatnou fyzickou kondici.
Někteří přítomní nejsou atleti.
Někteří přítomní mají špatnou fyzickou kondici.
d) Všechny kopce jsou zdolatelné.
Některé hory nejsou zdolatelné.
Některé hory nejsou kopce.
e) Všichni šimpanzi mohou vyřešit každý problém.
Existuje aspoň jeden problém.
Vyřeší-li šimpanz problém, dostane banán.
Alex je šimpanz.
Alex dostane banán.
Výsledek: a) Značí-li Z(x) . . . x je žák této třídy, H(x) . . . x je hudebník,
U(x) . . . x je umělec, úsudek odpovídá:
∀x (Z(x) ⇒ ¬H(x))
∀x (H(x) ⇒ U(x))
∀x (Z(x) ⇒ ¬U(x))
Marie Demlová: Příklady k předmětu Matem. logika 4. února 2008, 14:24
22 [080204-1424]
Úsudek není správný: Množina klausulí S = {¬Z(x) ∨ ¬H(x), ¬H(y) ∨
∨ U(y), Z(a), U(a)} je splnitelná. (Platí R (S) = S ∪ {¬H(a)}.)
b) Značí-li A(x) . . . x je atlet, K(x) . . . x nemá špatnou fyzickou kondici,
P(x) . . . x je přítomen, úsudek odpovídá:
∀x (A(x) ⇒ K(x))
∃x (P(x) ∧ A(x))
∃x (P(x) ∧ K(x))
Úsudek je správný, protože množina klausulí S = {¬A(x)∨K(x), P(a), A(a), ¬P(y)∨
∨ ¬K(y)}
je nesplnitelná. (Platí F ∈ R2
(S).)
c) Při stejném značení jako v minulém příkladě, úsudek odpovídá:
∀x (A(x) ⇒ K(x))
∃x (P(x) ∧ ¬A(x))
∃x (P(x) ∧ ¬K(x))
Úsudek není správný: Množina klausulí S = {¬A(x)∨K(x), P(a), ¬A(a), ¬P(y)∨
∨ K(y)} je splnitelná. (Platí R (S) = S ∪ {¬K(a), ¬A(x) ∨ ¬P(x)}.)
d) Značí-li K(x) . . . x je kopec, Z(x) . . . x je zdolatelný, H(x) . . . x je hora,
úsudek odpovídá:
∀x (K(x) ⇒ Z(x))
∃x (H(x) ∧ ¬Z(x))
∃x (H(x) ∧ ¬K(x))
Úsudek je správný, protože množina klausulí S = {¬K(x)∨Z(x), H(a), ¬Z(a), ¬H(y)∨
∨ K(y)}
je nesplnitelná. (Platí F ∈ R2
(S).)
e) Označme a konstantní symbol s významem . . . Alex, a vlastnosti: M(x)
. . . x je šimpanz, P(x) . . . x je problém, B(x) . . . x dostane banán a V (x, y)
. . . šimpanz x vyřeší problém y. Úsudek má tvar:
∀x (M(x) ⇒ ∀y (P(y) ⇒ V (x, y))
∃x P(x)
∀x ∀y ((M(x) ∧ P(y) ∧ V (x, y)) ⇒ B(x))
M(a)
B(a)
Úsudek je správný, protože množina klausulí
S = {¬M(x)∨¬P(y)∨V (x, y), P(b), ¬M(z)∨¬P(t)∨¬V (z, t)∨B(z), M(a), ¬B(a)}
je nesplnitelná. (Platí F ∈ R4
(S).)
Marie Demlová: Příklady k předmětu Matem. logika 4. února 2008, 14:24