Logika XI. RNDr. Kateˇrina Trlifajov´a PhD. Katedra teoretick´ e informatiky Fakulta informaˇ cn´ıch technologi´ı ˇ e vysok´ Cesk´ e uˇ cen´ı technick´ e v Praze c
Kateˇ rina Trlifajov´ a, 2010
BI-MLO, ZS 2011/12
Evropsk´ y soci´ aln´ı fond. Praha & EU: Investujeme do vaˇs´ı budoucnosti ˇ RNDr. Kateˇrina Trlifajov´ a PhD. (FIT CVUT)
Logika XI.
BI-MLO, ZS 2011/12
1 / 13
Logika X. Prenexn´ı norm´aln´ı tvar. Skolemizace. Rezoluˇcn´ı metoda.
ˇ RNDr. Kateˇrina Trlifajov´ a PhD. (FIT CVUT)
Logika XI.
BI-MLO, ZS 2011/12
2 / 13
Prenexn´ı norm´aln´ı tvar Definice Formule je v prenexn´ım norm´aln´ı tvaru, jestliˇze je ve tvaru (Q1 x1 )...(Qn xn )A, kde A je otevˇren´a formule, Qi jsou kvantifik´atory, xi jsou promˇenn´e. (∀x)(∀y )(∃z)(y < |x − y |), (∃k)(n = 2k)
Definice Formule B je varianta formule A, jestliˇze se liˇs´ı jen pˇrejmenov´an´ım v´azan´ych promˇenn´ych. (∀u)(∀v )(∃w )(w < |u − v |), (∃l)(n = 2l).
Vˇeta Je-li B varianta A, pak A ⇔ B. (∀x)(∀y )(∃z)(y < |x − y |) ⇔ (∀u)(∀v )(∃w )(w < |u − v |) ((∃k)(n = 2k) ⇔ (∃l)(n = 2l)) ˇ RNDr. Kateˇrina Trlifajov´ a PhD. (FIT CVUT)
Logika XI.
BI-MLO, ZS 2011/12
3 / 13
Prenexn´ı operace Chceme m´ıt formule v prenexn´ım tvaru. V´ıme: ((∀x)A ∧ (∀x)B) ⇔ (∀x)(A ∧ B) ((∃x)A ∨ (∃x)B) ⇔ (∃x)(A ∨ B)
Prenexn´ı operace 1
¬(∀x)A ⇔ (∃x)¬A ¬(∃x)A ⇔ (∀x)¬A
2
Nen´ı-li x voln´a v A, pak (A ∧ (∃x)B(x)) ⇔ (∃x)(A ∧ B(x)) (A ∨ (∀x)B(x)) ⇔ (∀x)(A ∨ B(x))
3
Nen´ı-li x voln´a v A, pak (A ⇒ (∀x)B(x)) ⇔ (∀x)(A ⇒ B(x)) (A ⇒ (∃x)B(x)) ⇔ (∃x)(A ⇒ B(x))
4
Nen´ı-li x voln´a v B, pak ((∀x)A(x) ⇒ B) ⇔ (∃x)(A(x) ⇒ B) ((∃x)A(x) ⇒ B) ⇔ (∀x)(A(x) ⇒ B)
ˇ RNDr. Kateˇrina Trlifajov´ a PhD. (FIT CVUT)
Logika XI.
BI-MLO, ZS 2011/12
4 / 13
Prenexn´ı operace - d˚ ukaz ad 2. Nen´ı-li x voln´a v A, pak (A ∨ (∀x)B(x)) ⇔ (∀x)(A ∨ B(x)). Dok´aˇzeme (A ∨ (∀x)B(x)) ⇒ (∀x)(A ∨ B(x)). Sporem. Kdyby ex. M tak, ˇze M |= (A ∨ (∀x)B(x)) ∧ ¬(∀x)(A ∨ B(x)), pak M |= (A ∨ (∀x)B(x)) a M |= (∃x)(¬A ∧ ¬B(x)), tedy existuje m ∈ M tak, ˇze ¬A ∧ ¬B[m], ale A ∨ B[m]. ⊥. Dok´aˇzeme (∀x)(A ∨ B(x)) ⇒ (A ∨ (∀x)B(x)). Sporem. Kdyby ex. M tak, ˇze M |= (∀x)(A ∨ B(x) ∧ ¬(A ∨ (∀x)B(x)), pak M |= (∀x)(A ∨ B(x)) a M |= ¬A a M |= (∃x)¬B(x), tedy existuje m ∈ M tak, ˇze ¬B[m], ale A ∨ B[m] a ¬A. ⊥. ad 3. Nen´ı-li x voln´a v A, pak (A ⇒ (∀x)B(x)) ⇔ (¬A ∨ (∀x)B(x)) ⇔ (∀x)(¬A ∨ B(x)) ⇔ (∀x)(A ⇒ B(x)) ad 4. Nen´ı-li x voln´a v B, pak ((∀x)A(x) ⇒ B) ⇔ (¬(∀x)A(x) ∨ B) ⇔ ((∃x)¬A(x) ∨ B) ⇔ (∃x)(A(x) ⇒ B) ˇ RNDr. Kateˇrina Trlifajov´ a PhD. (FIT CVUT)
Logika XI.
BI-MLO, ZS 2011/12
5 / 13
Prenexn´ı norm´aln´ı tvar Vˇeta Ke kaˇzd´e formuli existuje formule s n´ı ekvivalentn´ı v prenexn´ım norm´aln´ım tvaru. Pˇr´ıklady: 1
2
3
4
(∀a)(∀b)((a < b) ⇒ (∃c)(a < b < c) (∀a)(∀b)(∃c)((a < b) ⇒ (a < b < c) (∃x)(x = 0) ∧ (∃x)(x = S(0)) (∃x)(x = 0) ∧ (∃y )(y = S(0)) (∃x)(∃y )((x = 0) ∧ (y = S(0))) (∃x)(x > 0) ⇒ (∃y )(x + y > 0)) (∃z)(z > 0) ⇒ (∃y )(x + y > 0)) (∀z)(∃y )((z > 0) ⇒ (x + y > 0)) (∃y )(∀z)((z > 0) ⇒ (x + y > 0)) (∀)(( > 0) ⇒ (∃δ)(∀x)((δ > 0)∧(|x −c| < δ) ⇒ (|f (x)−f (c)| < )) (∀)(∃δ)(∀x)(( > 0) ⇒ ((δ > 0)∧(|x −c| < δ) ⇒ (|f (x)−f (c)| < ))
ˇ RNDr. Kateˇrina Trlifajov´ a PhD. (FIT CVUT)
Logika XI.
BI-MLO, ZS 2011/12
6 / 13
Skolemizace Chceme jen obecn´e kvantifik´atory.
Definice T 0 je konzervativn´ı rozˇs´ıˇren´ı teorie T , pr´avˇe kdyˇz L ⊆ L0 a pro kaˇzdou formuli jazyka L plat´ı T |= A, pr´avˇe kdyˇz T 0 |= A. (∃x)A(x) ... vybereme novou konstantu c L0 = L ∪ {c} T 0 = T ∪ {(∃x)A(x) ⇔ A(c)} (∀x)(∃y )A(x, y ) ... definujeme novou funkci f (x) L0 = L ∪ {f (x)} T 0 = T ∪ {(∀x)A(x, f (x))) ⇔ (∀x)(∃y )A(x, y )}
ˇ RNDr. Kateˇrina Trlifajov´ a PhD. (FIT CVUT)
Logika XI.
BI-MLO, ZS 2011/12
7 / 13
Skolem˚ uv norm´aln´ı tvar Vˇeta Ke kaˇzd´e uzavˇren´e formuli A existuje formule AS , kter´a je v prenexn´ım norm´aln´ı tvaru, kde vˇsechny kvantifik´atory jsou obecn´e, tzv. Skolem˚ uv norm´aln´ı tvar. A je splniteln´a, pr´avˇe kdyˇz AS je splniteln´a. Pˇr´ıklady: (∃y )(∀x)(x > y ) ... definujeme konstantu c tak, ˇze (∀x)(x > c) (∀x)(∃y )(x > y ) ... definujeme funkci f (x) tak, ˇze (∀x)(x > f (x)) (∃t)(∀x)(∀y )(∃z)(∀u)(∃w )A(t, x, y , z, u, w ) ... c (∀x)(∀y )(∃z)(∀u)(∃w )A(c, x, y , z, u, w ) ... g (x, y ) (∀x)(∀y )(∀u)(∃w )A(c, x, y , g (x, y ), u, w ) ... h(x, y , u) (∀x)(∀y )(∀u)A(c, x, y , g (x, y ), u, h(x, y , u)) ˇ RNDr. Kateˇrina Trlifajov´ a PhD. (FIT CVUT)
Logika XI.
BI-MLO, ZS 2011/12
8 / 13
Otevˇren´e j´adro formule Vˇeta Nechˇt A je otevˇren´a formule s voln´ymi promˇenn´ymi x1 , ..., xn . Potom pro libovolnou interpretaci M plat´ı M |= A, pr´avˇe kdyˇz M |= (∀x1 )...(∀xn )A. A je tautologie (∀x1 )...(∀xn )A je tautologie. A se naz´yv´a otevˇren´e j´adro formule (∀x1 )...(∀xn )A Pˇr´ıklad: (∀x)(∀y )((x > y ) ⇒ ¬(y > x)) je pravdiv´e v N, pr´avˇe kdyˇz (x > y ) ⇒ ¬(y > x) je pravdiv´e v N A(x) je tautologie, pr´avˇe kdyˇz (∀x)A(x) je tautologie. POZOR! A(x) ⇔ (∀x)A(x) nen´ı tautologie. A(x) ⇒ (∀x)A(x) nen´ı tautologie. (∀x1 )...(∀xn )A nen´ı logicky ekvivalentn´ı s A. ˇ RNDr. Kateˇrina Trlifajov´ a PhD. (FIT CVUT)
Logika XI.
BI-MLO, ZS 2011/12
9 / 13
Rezoluˇcn´ı metoda v predik´atov´e logice 1
Teorie. Konjunkce formul´ı.
2
Prenexn´ı norm´aln´ı tvar.
3
Skolemizace.
4
Otevˇren´e j´adro formule.
5
Klausule.
6
Resolventy formul´ı.
7
Kontradikce?
Pˇr´ıklad: (∀x)(P(x) ∨ Q(x)), (∃x)¬P(x) |= (∃x)Q(x) ? (∀x)(P(x) ∨ Q(x)) ∧ (∃x)¬P(x) ∧ ¬(∃x)Q(x) (∀x)(P(x) ∨ Q(x)) ∧ (∃z)¬P(z) ∧ (∀y )¬Q(y ) (∃z)(∀x)(∀y )((P(x) ∨ Q(x)) ∧ ¬P(z) ∧ ¬Q(y )) (∀x)(∀y )((P(x) ∨ Q(x)) ∧ ¬P(c) ∧ ¬Q(y )) (P(x) ∨ Q(x)) ∧ ¬P(c) ∧ ¬Q(y )) Q(c), ¬Q(c), ⊥ ˇ RNDr. Kateˇrina Trlifajov´ a PhD. (FIT CVUT)
Logika XI.
BI-MLO, ZS 2011/12
10 / 13
Rezoluˇcn´ı metoda v predik´atov´e logice
ˇ adn´y ˇclovˇek nen´ı zv´ıˇre Z´ Nˇekter´e zv´ıˇre je ˇselma. Tud´ıˇz nˇekter´a ˇselma nen´ı ˇclovˇek. (∀x)(c(x) ⇒ ¬z(x)), (∃x)(z(x) ∧ s(x)) |= (∃x)(s(x) ∧ ¬c(x)) (∀x)(¬c(x) ∨ ¬z(x)) ∧ (∃x)(z(x) ∧ s(x)) ∧ ¬(∃x)(s(x) ∧ ¬c(x)) (∀x)(¬c(x) ∨ ¬z(x)) ∧ (∃v )(z(v ) ∧ s(v )) ∧ ¬(∃u)(s(u) ∧ ¬c(u)) (∀x)(¬c(x) ∨ ¬z(x)) ∧ (z(K ) ∧ s(K )) ∧ (∀u)(s(u) ∧ ¬c(u)) (∀x)(∀u)(¬c(x) ∨ ¬z(x)) ∧ z(K ) ∧ s(K ) ∧ (¬s(u) ∨ c(u)) ((¬c(x) ∨ ¬z(x)) ∧ z(K ) ∧ s(K ) ∧ (¬s(u) ∨ c(u))) ... otevˇren´a formule s(K ), c(K ), ¬z(K ), z(K ), ⊥.
ˇ RNDr. Kateˇrina Trlifajov´ a PhD. (FIT CVUT)
Logika XI.
BI-MLO, ZS 2011/12
11 / 13
Pˇr´ıklady Kaˇzd´a vˇetˇs´ı ryba je rychlejˇs´ı neˇz menˇs´ı ryba. Tud´ıˇz jestliˇze je nˇejak´a ryba nejvˇetˇs´ı, pak je i nˇejak´a ryba nejrychlejˇs´ı, v (x, y ), r (x, y ) (∀x)(∀y )(v (x, y ) ⇒ r (x, y )) |= (∃z)(∀y )v (z, y ) ⇒ (∃z)(∀y )r (z, y ) Sporem: (∀x)(∀y )(v (x, y ) ⇒ r (x, y )) ∧ ¬((∃z)(∀u)v (z, u) ⇒ (∃z)(∀u)r (z, u)) (∀x)(∀y )(v (x, y ) ⇒ r (x, y )) ∧ (∃z)(∀u)v (z, u) ∧ ¬(∃s)(∀t)r (s, t) (∀x)(∀y )(¬v (x, y ) ∨ r (x, y )) ∧ (∃z)(∀u)v (z, u) ∧ (∀s)(∃t)¬r (s, t) RM: (∀x)(∀y )(¬v (x, y ) ∨ r (x, y )) ∧ (∀u)v (c, u) ∧ (∀s)¬r (s, f (s)) v (c, u), ¬r (c, f (c)), v (c, f (c)), ¬v (c, f (c)) ∨ r (c, f (c)). Spor. STROM: Tedy existuje c tak, ˇze (∀u)v (c, u). Tedy t´eˇz existuje d tak, ˇze ¬r (c, d). Tedy i v (c, d). Ale ¬v (c, d) ∨ r (c, d). Tedy spor. ˇ RNDr. Kateˇrina Trlifajov´ a PhD. (FIT CVUT)
Logika XI.
BI-MLO, ZS 2011/12
12 / 13
Pˇr´ıklad
Kaˇzd´y Cadillac je draˇzˇs´ı neˇz jak´ekoli levn´e vozidlo. Tud´ıˇz Cadillac nen´ı levn´e vozidlo, c(x), l(x) d(x, y ) (∀x)(∀y )((c(x) ∧ l(y )) ⇒ d(x, y )) |= (∀x)(c(x) ⇒ ¬l(x)) Kdyby tomu tak nebylo, pak (∀x)(∀y )((c(x) ∧ l(y ) ⇒ d(x, y ))) ∧ (∃x)(c(x) ∧ l(x)) Oznaˇcme si toto konkr´etn´ı auto m. Plat´ı c[m] ∧ l[m] ∧ ((¬c[m] ∨ ¬l[y ])) ∨ d[m, m]). Tedy d[m, m]. To je spor.
ˇ RNDr. Kateˇrina Trlifajov´ a PhD. (FIT CVUT)
Logika XI.
BI-MLO, ZS 2011/12
13 / 13
