Resolutsioon predikaatarvutuses

Idee on sama mis lausarvutuses: järelduse eituse lisame eeldustele ja näitame vastuolu – toome tühja klausli □. Uut on see, et valemites on kvantorid ja muutujad: need tuleb enne resolutsiooni eemaldada (Skolemi vorm) ja samm-sammul asendustega ühitada.

Samm 1 · Too valemid Skolemi klauslikujule

Iga valem töödeldakse läbi kuue alamsammu:

  1. Eemalda implikatsioonid ja ekvivalentsid: X → Y ≡ ¬X ∨ Y
  2. Vii eitused sisse: ¬∀x F ≡ ∃x ¬F, ¬∃x F ≡ ∀x ¬F, De Morgan, ¬¬F ≡ F
  3. Nimeta muutujad ümber nii, et igal kvantoril oleks oma muutuja
  4. Preneksne kuju: kõik kvantorid valemile ette
  5. Skolemi vorm: eemalda kõik ∃-kvantorid (vt allpool)
  6. Klauslikuju: järelejäänud ∀-muutujad jäetakse lihtsalt ära; jaota konjunktsioonid eraldi klausliteks

Skolemi reegel – kuidas ∃ eemaldada?

∃x P(x)
⇒
P(c)

Kui ∃ ees pole ühtegi ∀: asenda muutuja uue Skolemi konstandiga (nt c, a).

∀x ∃y L(x, y)
⇒
L(x, f(x))

Kui ∃y ees on üks ∀-muutuja: asenda y Skolemi funktsiooniga ühest muutujast f(x) – „see, kes x-i kohta leidub“.

∀x ∀y ∃z S(x, y, z)
⇒
S(x, y, g(x, y))

Kui ∃z ees on kaks ∀-muutujat: Skolemi funktsioon kahest muutujast g(x, y). Üldjuhul: nii palju argumente kui ees olevaid ∀-muutujaid.

Samm 2 · Lisa järelduse eitus

Järeldus on tavaliselt kujul ∃y F(y). Tema eitus: ¬∃y F(y) ≡ ∀y ¬F(y) – eituses jääb ∀-muutuja alles ja Skolemit ei teki! Ka eitus viiakse klauslikujule.

Samm 3 · Asendus ja resolutsioonisamm

Kaks literaali saab taandada, kui üks on P(...) ja teine ¬P(...) ning argumentide saab asendusega σ võrdseks teha. Asendus kirjutatakse σ = {x/t} – „muutuja x asemele term t“. Resolventi kantakse asendus kaasa:

P(x) ∨ X
¬P(t) ∨ Y
⊢
(X ∨ Y) σ

Tähtis: erinevates klauslites võivad olla samanimelised muutujad, kuid need on omavahel sõltumatud – iga klausli muutujaid võib asendada eraldi.

Näide tervikuna (ilma Skolemi funktsioonita)

„Iga inimene on surelik. Sokrates on inimene.“ Tõesta: Sokrates on surelik.   I(x) = x on inimene, S(x) = x on surelik, s = Sokrates

(1) ∀x (I(x) → S(x)) ⇒ ¬I(x) ∨ S(x) · (2) I(s) · järeldus S(s), eitus (3) ¬S(s). Skolemi funktsiooni ei teki, sest ∃-kvantoreid pole.

¬I(x) ∨ S(x) (1)
I(s) (2)
S(s)
¬S(s) (3)
□
σ₁ = {x/s}
σ₂ = { } (pole vaja)
(1)+(2): taandub I
+(3): taandub S

Tekkis □ ⇒ vastuolu ⇒ „Sokrates pole surelik“ on võimatu ⇒ Sokrates on surelik.

Ülesanne 1 · Puu ilma Skolemi funktsioonita

Ülesanne. „Iga programmeerija armastab loogikat. Anne on programmeerija.“ Tõesta: Anne armastab loogikat.

P(x) = x on programmeerija, L(x) = x armastab loogikat, a = Anne. Siin on ainult ∀-kvantor ja järelduse eitus, seega Skolemi funktsiooni ei teki.

A · Paiguta klauslid väidete juurde

Lohista kiip kasti – või puuduta kiibi ja siis kasti (mobiilis). Puuduta kastis olevat kiipi, et see tagasi kandikule viia.

¬P(x) ∨ L(x) P(a) ¬L(a)
„Iga programmeerija armastab loogikat“ ∀x (P(x) → L(x))
„Anne on programmeerija“
„Järelduse eitus: Anne ei armasta loogikat“

Ülesanne 2 · Üks muutuja ja Skolemi funktsioon

Ülesanne. „Igal kassil on omanik. Miisu on kass.“ Tõesta: Miisul on omanik.

K(x) = x on kass, O(x, y) = y on x-i omanik, m = Miisu.

Skolemi samm: ∀x (K(x) → ∃y O(x, y)) ⇒ ∀x (¬K(x) ∨ O(x, o(x))) – kuna ∃y ees on üks ∀-muutuja, asendub y Skolemi funktsiooniga o(x) („x-i omanik“).

Klauslid: (1) ¬K(x) ∨ O(x, o(x)) · (2) K(m) · järeldus ∃y O(m, y), eitus ∀y ¬O(m, y) ⇒ (3) ¬O(m, y).

Lehed on antud. Kirjuta tühjadesse kastidesse resolvent, tühi klausel ja mõlema sammu asendused σ₁ ja σ₂. Vajadusel vihje ühe kaupa.

Klaviatuur:
¬K(x) ∨ O(x, o(x)) (1)
K(m) (2)
¬O(m, y) (3)
σ₁={x/}
σ₂={y/}

Ülesanne 3 · Kaks muutujat ja Skolemi funktsioon

Ülesanne. „Kui x võidab y-t, siis saab x y käest preemia. Juss võitis Matit.“ Tõesta: Juss sai Matilt preemia.

V(x, y) = x võidab y-t, P(x, y, z) = x saab y käest preemia z, j = Juss, m = Mati.

Skolemi samm: ∀x ∀y (V(x, y) → ∃z P(x, y, z)) – kuna ∃z ees on kaks ∀-muutujat, tekib kahekohaline Skolemi funktsioon p(x, y) („preemia, mille x y-lt saab“). Järeldus on ∃z P(j, m, z) ja tema eitus ∀z ¬P(j, m, z).

Siin pole ühtegi kasti ette antud: kirjuta kõik klauslid, resolvent, tühi klausel ja asendused. „Vihje“ avab korraga ühe kasti – samm kaupa.

Klaviatuur:
σ₁={x/, y/}
σ₂={z/}