10 [070508-1526]
2.3 Rezoluční metoda ve výrokové logice
2.3.1 Příklad. Najděte rezolventy klausulí
a) x ∨ ¬y ∨ z a ¬x ∨ z ∨ ¬t;
b) a ∨ b a ¬b ∨ c;
c) p ∨ q ∨ r ∨ ¬s a p ∨ q ∨ s ∨ ¬t.
Výsledek. a) ¬y ∨ z ∨ ¬t; b) a ∨ c; c) p ∨ q ∨ r ∨ ¬t.
2.3.2 Příklad. Utvořte R2
(S) pro S = {¬a ∨ b, ¬b ∨ c, a ∨ d, a ∨ ¬c, a ∨ ¬d}.
Výsledek. R2
(S) = {¬a ∨ b, ¬b ∨ c, a ∨ d, a ∨ ¬c, a ∨ ¬d, ¬a ∨ c, b ∨ d, b ∨
∨ ¬c, b ∨ ¬d, a, a ∨ ¬b, c, b, b ∨ ¬b, a ∨ ¬a, c ∨ d, c ∨ ¬c, c ∨ ¬d, a ∨ b}.
2.3.3 Příklad. Rezoluční metodou rozhodněte, zda S je splnitelná množina
klausulí, kde:
a) S = {p ∨ q ∨ r, ¬p ∨ s ∨ t, ¬s ∨ y, ¬t, ¬p ∨ ¬x, ¬q ∨ w, ¬q ∨ ¬w};
b) S = {a, ¬a ∨ ¬b ∨ c, ¬a ∨ ¬d ∨ f, ¬d ∨ b, ¬c ∨ g, ¬f ∨ g, ¬g};
c) S = {x ∨ y, ¬z ∨ t, ¬x ∨ t, ¬y ∨ z, ¬t}.
Výsledek. a) Splnitelná. Je pravdivá např. pro ohodnocení u(p) = 1, u(q) =
= 0, u(s) = 1, u(x) = 0, u(y) = 1, u(r), u(t) a u(w) libovolné.
b) Splnitelná. Je pravdivá např. pro ohodnocení u(a) = 1, u(b) = u(c) =
= u(d) = u(f) = u(g) = 0.
c) Nesplnitelná.
2.3.4 Příklad. Rezoluční metodou rozhodněte, zda S je splnitelná množina
formulí, kde:
a) S = {p ⇒ (r ∨ s), ¬p ⇒ q, r ⇒ (t ∧ v), (v ∧ t) ⇒ s};
b) S = {a ⇒ (b ∧ f), (a ∧ b) ⇒ c, c ⇒ (f ∧ (¬d ∨ f)), a};
Výsledek. a) Splnitelná. Je pravdivá např. pro ohodnocení u(p) = 1, u(r) =
= 0, u(s) = 1, u(q), u(t) a u(v) libovolné.
b) Splnitelná. Je pravdivá např. pro ohodnocení u(a) = u(b) = u(c) =
= u(f) = 1, u(d) libovolné.
2.3.5 Příklad. Pomocí rezoluční metody rozhodněte, zda množina formulí S
je splnitelná a zda S |= α, kde:
a) S = {x ⇒ y, y ⇒ (z ∨ ¬x), ¬t ⇒ (x ∧ ¬z), t ⇒ x}, α = z;
b) S = {p, (p ∧ r) ⇒ s, (p ∧ q) ⇒ t, q ⇒ r, (s ∨ t) ⇒ w}, α = w.
Výsledek. a) S je splnitelná (např. u(x) = u(y) = u(z) = 1); S |= z.
b) S je splnitelná (např. u(p) = 1, u(q) = u(r) = u(s) = u(t) = u(w) = 0);
S |= w.
Marie Demlová: Příklady k předmětu Matem. logika 8. května 2007, 15:26
2.3. Rezoluční metoda ve výrokové logice [070508-1526] 11
2.3.6 Příklad. Formalizujte následující věty. Pomocí rezoluční metody rozhodněte,
zda věta pod čarou je sémantickým důsledkem vět nad čarou:
a) Jestliže bude pršet, nepůjdeme na výpravu.
Jestliže nepůjdeme na výpravu, půjdeme do kina.
Půjdeme-li do kina a bude pršet, pojedeme autobusem.
Pojedeme-li autobusem, budeme potřebovat peníze.
Bude pršet.
Budeme potřebovat peníze.
b) Na zájezd do Řecka pojede Petr nebo Pavel.
Jestliže pojede Pavel, pojede Simona a nepojede Renata.
Jestliže pojede Tomáš, pojede i Renata.
Jestliže pojede Simona, pojede Tomáš.
Petr pojede na zájezd do Řecka.
Výsledek. a) Platí.
{p ⇒ ¬v, ¬v ⇒ k, (k ∧ p) ⇒ a, a ⇒ m, p} |= m,
kde p je výrok „bude pršet , v „půjdeme na výpravu , k „půjdeme do kina , a
„pojedeme autobusem , m „budeme potřebovat peníze .
b) Platí.
{e ∨ a, a ⇒ (s ∧ ¬r), t ⇒ r, s ⇒ t} |= e,
kde e je výrok „na zájezd pojede Petr , a „na zájezd pojede Pavel , s „na zájezd
pojede Simona , r „na zájezd pojede Renata , t „na zájezd pojede Tomáš .
Marie Demlová: Příklady k předmětu Matem. logika 8. května 2007, 15:26