решение задач по мат. логике (2009) (1162148), страница 2
Текст из файла (страница 2)
Рассмотрим ее на интерпретации, область которойсодержит три элемента. На данной интерпретации формула истинна. То есть для любой подстановки онаистинна. Следовательно существует подстановка, состоящая из 1 или 2 объектов, на которой формула также истинна. Следовательно формула истинна на интерпретации, область которой содержит только эти2 объекта, следовательно такой формулы нет.Упражнение 2.5 Данная задача была решена некорректно.103Нормальные формы и унификация3.1Преведение к ССФ1.
Переименование переменных|= ∃∀ x F (x) ≡ ∃∀ y F (y)2. Уничтожение импликаций |= (A → B) ≡ (¬A ∨ B)3. Отрицания∨(a) |= ¬(A &∨ B) ≡ (¬A & ¬B)(b) |= (¬ ∃∀ xF (x)) ≡ ( ∀∃ x¬F (x)(c) |= ¬¬A ≡ A4. Вынос кванторов|= ∃∀ xF (x) &∨ B ≡∃ x(F (x) &∨∀B)5. |= A & B ∨ C ≡ (A ∨ C) & (B ∨ C)3.2Нахождение НОУP (t1 , t2 , .
. . tn )= P (s1 , s2 , . . . sn )t1 = s1t2 = s2..........tn = sn→1.f (t1 , t2 , . . . tn )= f (s1 , s2 , . . . sn )→t1 = s1t2 = s2..........tn = sn2.f (t1 , t2 , . . . tn )= f (s1 , s2 , . . . sk )→НОУ не существует3. ti = xi→x1 = t i4. ti = ti→∅5. xi = ti(xi ∈/ V arti , ∃k xi ∈ V artk )6. xi = ti(xi ∈ V arti )3.3(ti 6= xi )→→Во все tk подствить вместо xi tiНОУ не существуетЗадачиУпражнение 3.11. ∃x∀y P (x, y) & ∀x∃y P (y, x)1∃x∀y P (x, y) & ∀x∃y P (y, x) −→ ∃x1 ∀y1 P (x1 , y1 ) & ∀x2 ∃y2 P (y2 , x2 )4∃x1 ∀y1 P (x1 , y1 ) & ∀x2 ∃y2 P (y2 , x2 ) −→ ∃x1 ∀y1 ∀x2 ∃y2 P (x1 , y1 ) & P (y2 , x2 )2.
∀x((∃y P (y, x) → ∃y P (x, y)) → Q(x)) → ∃x Q(x)1∀x((∃y P (y, x) → ∃y P (x, y)) → Q(x)) → ∃x Q(x) −→2,3∀x1 ((∃y1 P (y1 , x1 ) → ∃y2 P (x1 , y2 )) → Q(x1 )) → ∃x2 Q(x2 ) −→4∃x1 ((∀y1 ¬P (y1 , x1 ) ∨ ∃y2 P (x1 , y2 )) & ¬Q(x1 )) ∨ ∃x2 Q(x2 ) −→5∃x1 ∀y1 ∃y2 ∀x2 ((¬P (y1 , x1 ) ∨ P (x1 , y2 )) & ¬Q(x1 ) ∨ Q(x2 )) −→∃x1 ∀y1 ∃y2 ∀x2 ((¬P (y1 , x1 ) ∨ P (x1 , y2 ) ∨ Q(x2 )) & (¬Q(x1 ) ∨ Q(x2 )))113. ¬∀y (∃x P (x, y) → ∀u (R(y, u) → ∀z (P (z, u) ∨ ¬R(z, y))))2,3¬∀y (∃x P (x, y) → ∀u (R(y, u) → ∀z (P (z, u) ∨ ¬R(z, y)))) −→4∃y (∃x P (x) & (∃u(R(z, u) & ∀z (P (z, u) ∨ ¬R(z, y))))) −→∃y∃x∃u∀z (P (x, y) & R(y, u) & (P (z, u) ∨ R(z, y)))4.
∃x∃y (P (x, y) → R(x)) → ∀x (¬∃y P (x, y) ∨ R(x))1∃x∃y (P (x, y) → R(x)) → ∀x (¬∃y P (x, y) ∨ R(x)) −→2,3∃x1 ∃y1 (P (x1 , y1 ) → R(x1 )) → ∀x2 (¬∃y2 P (x2 , y2 ) ∨ R(x2 )) −→4∀x1 ∀x2 (P (x1 , y2 ) & ¬R(x1 )) ∨ ∀x2 (∀y2 ¬P (x2 , y2 ) ∨ R(x2 )) −→5∀x1 ∀x2 ∀x2 ∀y2 (P (x1 , y2 ) & ¬R(x1 ) ∨ ¬P (x2 , y2 ) ∨ R(x2 )) −→∀x1 ∀x2 ∀x2 ∀y2 ((P (x1 , y2 ) ∨ ¬P (x2 , y2 ) ∨ R(x2 )) & (¬R(x1 ) ∨ ¬P (x2 , y2 ) ∨ R(x2 )))5.
∃x∀y (P (x, y) → (¬P (y, x) → (P (x, x) → P (y, y)) &(P (y, y) → P (x, x))))2,3∃x∀y (P (x, y) → (¬P (y, x) → (P (x, x) → P (y, y)) &(P (y, y) → P (x, x)))) −→5∃x∀y (¬P (x, y) ∨ P (y, x) ∨ (¬P (x, x) ∨ P (y, y)) & (¬P (y, y) ∨ P (x, x))) −→∃x∀y ((¬P (x, y) ∨ P (y, x) ∨ ¬P (x, x) ∨ P (y, y)) & (¬P (x, y) ∨ P (y, x) ∨ ¬P (y, y) ∨ P (x, x)))6. ∃x (∀x P (x, x) ∨ ∃x ¬R(x)) → ∃x (R(x) → ∃y P (f (x), y))1∃x (∀x P (x, x) ∨ ∃x ¬R(x)) → ∃x (R(x) → ∃y P (f (x), y)) −→2,3∃k (∀x1 P (x1 , x1 ) ∨ ∃x2 ¬R(x2 )) → ∃x3 (R(x3 ) → ∃y P (f (x3 ), y)) −→4∃k (∃x1 ¬P (x1 , x1 ) & ∀x2 ¬R(x2 ) ∨ ∃x3 (¬R(x3 ) ∨ ∃y R(f (x3 ), y))) −→5∃k∃x1 ∀x2 ∃x3 ∃y (¬P (x1 , x1 ) & ¬R(x2 ) ∨ ¬R(x3 ) ∨ R(f (x3 ), y)) −→∃k∃x1 ∀x2 ∃x3 ∃y ((¬P (x1 , x1 ) ∨ ¬R(x3 ) ∨ R(f (x3 ), y)) & (¬R(x2 ) ∨ ¬R(x3 ) ∨ R(f (x3 ), y)))Упражнение 3.21.
∀x∃y∀z∃u R(x, y, z, u)∀x∃y∀z∃u R(x, y, z, u) −→∀x∀z∃u R(x, f (x), z, u) −→∀x∀z R(x, f (x), z, g(x, z))2,32. ¬∀x (∃y R(x, y) → ∀z P (z, x)) −→4∃z (∃y R(x, y) &∃z ¬P (z, x)) −→∃x∃y∃z (R(x, y) & ¬P (z, x)) −→∃y∃z (R(c1 , y) & ¬P (z, c1 )) −→∃z (R(c1 , c2 ) & ¬P (z, c1 )) −→R(c1 , c2 ) & ¬P (3 , c1 )3. ¬∀y (∃x P (x, y) → ∀u (R(y, u) → ∀z (P (z, u) ∨ ¬R(z, y))))2,3¬∀y (∃x P (x, y) → ∀u (R(y, u) → ∀z (P (z, u) ∨ ¬R(z, y)))) −→4∃y (∃x P (x) & (∃u(R(z, u) & ∀z (P (z, u) ∨ ¬R(z, y))))) −→∃y∃x∃u∀z (P (x, y) & R(y, u) & (P (z, u) ∨ R(z, y))) −→∃x∃u∀z (P (x, c1 ) & R(c1 , u) & (P (z, u) ∨ R(z, c1 ))) −→∃u∀z (P (c2 , c1 ) & R(c1 , u) & (P (z, u) ∨ R(z, c1 ))) −→∀z (P (c2 , c1 ) & R(c1 , c3 ) & (P (z, c3 ) ∨ R(z, c1 )))4.
∃x∃y (P (x, y) → R(x)) → ∀x (¬∃y P (x, y) ∨ R(x))1∃x∃y (P (x, y) → R(x)) → ∀x (¬∃y P (x, y) ∨ R(x)) −→122,3∃x1 ∃y1 (P (x1 , y1 ) → R(x1 )) → ∀x2 (¬∃y2 P (x2 , y2 ) ∨ R(x2 )) −→4∀x1 ∀x2 (P (x1 , y2 ) & ¬R(x1 )) ∨ ∀x2 (∀y2 ¬P (x2 , y2 ) ∨ R(x2 )) −→5∀x1 ∀x2 ∀x2 ∀y2 (P (x1 , y2 ) & ¬R(x1 ) ∨ ¬P (x2 , y2 ) ∨ R(x2 )) −→∀x1 ∀x2 ∀x2 ∀y2 ((P (x1 , y2 ) ∨ ¬P (x2 , y2 ) ∨ R(x2 )) & (¬R(x1 ) ∨ ¬P (x2 , y2 ) ∨ R(x2 )))5. ∃x∀y (P (x, y) → (¬P (y, x) → (P (x, x) → P (y, y)) &(P (y, y) → P (x, x))))2,3∃x∀y (P (x, y) → (¬P (y, x) → (P (x, x) → P (y, y)) &(P (y, y) → P (x, x)))) −→5∃x∀y (¬P (x, y) ∨ P (y, x) ∨ (¬P (x, x) ∨ P (y, y)) & (¬P (y, y) ∨ P (x, x))) −→∃x∀y ((¬P (x, y) ∨ P (y, x) ∨ ¬P (x, x) ∨ P (y, y)) & (¬P (x, y) ∨ P (y, x) ∨ ¬P (y, y) ∨ P (x, x))) −→∀y ((¬P (c, y) ∨ P (y, c) ∨ ¬P (c, c) ∨ P (y, y)) & (¬P (c, y) ∨ P (y, c) ∨ ¬P (y, y) ∨ P (c, c)))6.
∃x (∀x P (x, x) ∨ ∃x ¬R(x)) → ∃x (R(x) → ∃y P (f (x), y))1∃x (∀x P (x, x) ∨ ∃x ¬R(x)) → ∃x (R(x) → ∃y P (f (x), y)) −→2,3∃k (∀x1 P (x1 , x1 ) ∨ ∃x2 ¬R(x2 )) → ∃x3 (R(x3 ) → ∃y P (f (x3 ), y)) −→4∃k (∃x1 ¬P (x1 , x1 ) & ∀x2 ¬R(x2 ) ∨ ∃x3 (¬R(x3 ) ∨ ∃y R(f (x3 ), y))) −→5∃k∃x1 ∀x2 ∃x3 ∃y (¬P (x1 , x1 ) & ¬R(x2 ) ∨ ¬R(x3 ) ∨ R(f (x3 ), y)) −→∃k∃x1 ∀x2 ∃x3 ∃y ((¬P (x1 , x1 ) ∨ ¬R(x3 ) ∨ R(f (x3 ), y)) & (¬R(x2 ) ∨ ¬R(x3 ) ∨ R(f (x3 ), y))) −→∃x1 ∀x2 ∃x3 ∃y ((¬P (x1 , x1 ) ∨ ¬R(x3 ) ∨ R(f (x3 ), y)) & (¬R(x2 ) ∨ ¬R(x3 ) ∨ R(f (x3 ), y))) −→∀x2 ∃x3 ∃y ((¬P (c1 , c1 ) ∨ ¬R(x3 ) ∨ R(f (x3 ), y)) & (¬R(x2 ) ∨ ¬R(x3 ) ∨ R(f (x3 ), y))) −→∀x2 ∃y ((¬P (c1 , c1 ) ∨ ¬R(g(x2 )) ∨ R(g(x2 ), y)) & (¬R(x2 ) ∨ ¬R(g(x2 )) ∨ R(f (g(x2 )), y))) −→∀x2 ((¬P (c1 , c1 ) ∨ ¬R(g(x2 )) ∨ R(g(x2 ), h(x2 )) & (¬R(x2 ) ∨ ¬R(g(x2 )) ∨ R(f (g(x2 )), h(x2 ))))Упражнение 3.3 Данная задача не рассматривалась на семинарах. Если будет время, ее решение будетдобавленно.
Если пришлете мне решение данной задачи, оно появится тут скорее ;-).Упражнение 3.41. P (c, X, f (X))P (c, Y, Y )c= cX= Yf (X) = YXY==4Yf (X)5 XZV===YYg(Y )VYg(Y )h(Z, Y )=Y= f (Y )3−→НОУ НетP (f (Y, X), g(Y ), V ) f (X, Y ) = f (Y, X)Z=g(Y )h(Z, Y ) =VX=Y=Z=h(Z, Y ) =XY−→2. P (f (X, Y ), Z, h(Z, Y ))X= Yf (X) = Y−→1−→4−→3−→X=YY=XZ= g(Y )h(Z, Y ) =VX=Z=h(Z, Y ) = XZVYg(Y )V=Y=g(Y )= h(g(Y ), Y )131−→3−→НОУ построен3. R(Z, f (X, b, Z))R(h(X), f (g(a), Y, Z))Z=h(X)f (X, b, Z) = f (g(a), Y, Z) ZXb===h(X)g(a)Y ZXY===h(g(a))g(a)b ZXY3−→X=f (Y )f (Y )=Xh(Z, X) = h(f (Y ), f (Z)) XZY===f (Y )f (Y )f (Y )f (Z)f (Y )f (Y )Z= h(X)= g(a)=bh(X)g(a)YZ4−→5−→P (f (Y ), X, h(f (Y ), f (Z)))X=f (Y ) =Z=f (Y ) =−→====НОУ построен4.
P (X, f (Y ), h(Z, X))1ZXbZX= f (Y )Z= f (Y )f (Y ) = f (Z)455. P (X1 , X2 , X3 .X4 )X=f (Y ) == ZX=−→−→1−→ XZY= f (Y )= f (Z)=Zf (Y )Xf (Y )f (Z)5−→1−→НОУ НетP (f (c, c), f (X1 , X1 ), f (X2 , X2 ), f (X3 , X3 ))X1X2X3X4X1X2X3X4=f (c, c)= f (X1 , X1 )= f (X2 , X2 )= f (X3 , X3 )X1X2X3X4=f (c, c)=f (f (c, c), f (c, c))= f (f (f (c, c), f (c, c)), f (f (c, c), f (c, c)))=f (X3 , X3 )X1X2X3X4=f (c, c)=f (f (c, c), f (c, c))=f (f (f (c, c), f (c, c)), f (f (c, c), f (c, c)))= f (f (f (f (c, c), f (c, c)), f (f (c, c), f (c, c))), f (f (f (c, c), f (c, c)), f (f (c, c), f (c, c))))5−→=f (c, c)= f (f (c, c), f (c, c))=f (X2 , X2 )=f (X3 , X3 )5−→5−→14НОУ построен4Метод резолюцийУпражнение 4.11.
¬P (f (x, y), z, h(z, y)) ∨ R(z, v), Q(x) ∨ P (f (y, x), g(y), v)D1 = ¬P (f (x, y), z, h(z, y)) ∨ R(z, v)D2 = Q(x) ∨ P (f (y, x), g(y), v)НОУ(P (f (y, x), g(y), v), ¬P (f (x, y), z, h(z, y))) f (y, x) = f (x, y) f (y, x) = f (x, y)3g(y)=zz=g(y)−→v== h(z, y)v== h(z, y)yxzv==x=y=g(y)= h(z, y)=x=g(x)= h(z, x)yzv=5yxzv==x=x=g(x)= h(z, x)5=x=g(x)= h(g(x), x)−→−→yzv=1−→4−→Θ = {y/x, z/g(x), v/h(g(x), x)}D3D1 ,D2=ΘR(g(x), h(g(x), x)) ∨ Q(x)2. P (x, y, h(y, x)) ∨ R(y, f (x)), ¬P (x, f (x), h(x, y)) ∨ P (y, g(x), h(y, y))D1 = P (x1 , y1 , h(y1 , x1 )) ∨ R(y1 , f (x1 ))D2 = ¬P (x2 , f (x2 ), h(x2 , y2 )) ∨ P (y2 , g(x2 ), h(y2 , y2 ))НОУ(P (x1 , y1 , h(y1 , x1 )), ∨ P (y2 , g(x2 ), h(y2 , y2 )))x1 =y2x=y12y1 = g(x2 )1y1=g(x2 )−→y1 =y2h(y1 , x1 ) = h(y2 , y2 )x1 =y2y2y1y1x1=x1= g(x2 )=y2=y2 y2y1y1=== x1y1y2=y2= g(x2 )= g(x2 )x1g(x2 )y25−→3−→5−→y2y1y1x1====x1g(x2 )x1x1−→ x1y1y2=y2= g(x2 )=y1−→ x1y1y2= g(g2 )= g(x2 )= g(x2 )3−→45Θ = {x1 /g(x2 ), y1 /g(x2 ), y2 /g(x2 )}D3D1 ,D2=ΘR(g(x2 ), f (g(x2 ))) ∨ ¬P (x2 , f (x2 ), , h(x2 , g(x2 )))15Упражнение 4.21.
S = {D1 , D2 , D3 , D4 , D5 }D1D2D3D4D5= P (X1 , f (X1 ))= R(Y2 , Z2 ) ∨ ¬P (Y2 , f (a))= ∨R(c, X3 )= R(X4 , Y4 ) ∨ R(Z4 , f (Z4 )) ∨ ¬P (Z4 , Y4 )= P (X5 , X5 )D6D1 ,D2={X1 /a,Y2 /a}D7D4={X4 /Z4 ,Y4 /f (Z4 )}D8D7 ,D3={X3 /f (c),Z7 /c}D9D1 ,D8={X1 /c}R(a, Z6 )R(Z7 , f (Z7 )) ∨ ¬P (Z7 , f (Z7 ))¬P (c, f (c))2. S = {D1 , D2 .D3 , D4 , D5 , D6 , D7 }D1D2D3D4D5D6D7= E(x1 ) ∨ V (y1 ) ∨ C(f (x1 ))= E(x2 ) ∨ S(x2 , f (x2 ))= ¬E(a)= P (a)= P (f (x5 )) ∨ ¬S(y5 , z5 )= ¬P (x6 ) ∨ ¬V (g(x6 )) ¬ ∨ V (y6 )= ¬P (x7 ) ∨ ¬C(y7 )D8D6={y6 /g(x)}D9D4 ,D7={x7 /a}¬P (x8 ) ∨ ¬V (g(x8 ))¬C(y9 )D10D8 ,D4={x8 /a}D11D1 ,D9={y9 /f (x1 )}E(x11 ) ∨ V (y11 )D12D11 ,D10={y11 /g(a))}E(x12 )D13D12 ,D3={x12 /a}¬V (g(a))3.














