решение задач по мат. логике (2009) (1162148), страница 3
Текст из файла (страница 3)
S = {D1 , D2 , D3 , D4 }D1D2D3D4= P (y1 , f (x1 ))= ¬Q(y2 ) ∨ ¬Q(z2 ) ∨ ¬P (y, f (z)) ∨ Q(v)= Q(b)= ¬Q(a)D5D1 ,D2={x1 /z2 ,y1 /y2 }D6D5={z5 /y5 }D7D6 ,D4={v6 /a}¬Q(y7 )D8D7 ,D3={y7 /b}¬Q(y5 ) ∨ ¬Q(z5 ) ∨ Q(v5 )¬Q(y6 ) ∨ Q(v6 )16Упражнение 4.31. ∃x P (x) → ¬∀x ¬P (x)φ0 = ¬(∃x P (x) → ¬∀y ¬P (x))φ01 = ∃x P (x) & ∀y ¬P (y)φ02 = ∃x∀y P (x) & ¬P (y)φ1 = ∀y P (c) & ¬P (y)S = {P (c), ¬P (y)}D1 = P (c)D2 = ¬P (y)D3D1 ,D2={y/c}2. ∃x∀yR(x, y) → ∀y∃xR(x, y)φ0 = ¬(∃x1 ∀y1 R(x1 , y1 ) → ∀y2 ∃x2 R(x2 , y2 ))φ01 = ∃x1 ∀y1 R(x1 , y1 ) & ∃y2 ∀x2 ¬R(x2 , y2 )φ02 = ∃x1 ∀y1 ∃y2 ∀x2 R(x1 , y1 ) & ¬R(x2 , y2 )φ1 = ∀y1 ∀x2 R(c, y1 ) & ¬R(x2 , f (y1 ))S = {R(c, y1 ), ¬R(x2 , f (y1 ))}D1 = R(c, y1 )D2 = ¬R(x2 , f (y2 ))D3D1 ,D2={x2 /c,y1 /f (y2 )}переименование переменных3.
∀x(P (x) → ∃y R(x, f (y))) → (∃x ¬P (x) ∨ ∀x∃zR(x, z))φ0 = ¬(∀x1 (P (x1 ) → ∃y1 R(x,1 f (y1 ))) → (∃x2 ¬P (x2 ) ∨ ∀x3 ∃z1 R(x3 , z1 )))φ01 = ∀x1 (¬P (x1 ) ∨ ∃y1 R(x1 , f (y1 ))) & ∀x2 P (x2 ) & ∃x3 ∀z1 ¬R(x3 , z1 )φ02 = ∀x1 ∃y1 ∀x2 ∃x3 ∀z1 (¬P (x1 ) ∨ R(x1 , f (y1 ))) & P (x2 ) & ¬R(x3 , z1 )φ1 = ∀x1 ∀x2 ∀z1 (¬P (x1 ) ∨ R(x1 , f (g(x1 )))) & P (x2 ) & ¬R(h(x1 , x2 ), z1 )S = {¬P (x1 ) ∨ R(x1 , f (g(x1 ))), P (x2 ), ¬R(h(x1 , x2 ), z1 )}D1 = ¬P (x1 ) ∨ R(x1 , f (g(x1 )))D2 = P (x2 )D3 = ¬R(h(x31 , x32 ), z3 )D4D1 ,D2={x1 /x2 }D5D3 ,D4={x4 /h(x31 ,x32 ),z3 /f (g(h(x31 ,x32 )))}R(x4 , f (g(x4 ))4.
∀x∃y∀z(P (x, y) → P (y, z))φ0 = ¬(∀x∃y∀z(P (x, y) → P (y, z)))φ01 = ∃x∀y∃z(P (x, y) & ¬P (y, z)))φ1 = ∀y(P (c, y) & ¬P (y, f (y)))S = {P (c, y), ¬P (y, f (y))}D1 = P (c, y1 )D2 = ¬P (y2 , f (y2 ))D3D1 ,D2={y2 /c,y1 /f (c)}175. ∃x∀y∃z(P (x, y) → P (y, z))φ0 = ¬(∃x∀y∃z(P (x, y) → P (y, z)))φ01 = ∀x∃y∀z(P (x, y) & ¬P (y, z)))φ02 = ∀x∀z(P (x, f (x)) & ¬P (y, z)))S = {P (x, f (x)), ¬P (y, z)}D1 = P (x1 , f (x1 ))D2 = ¬P (y2 , z2 )D3D1 ,D2={y2 /x1 ,z2 /f (x1 )}6. ∃x∀y(∀z(P (y, z) → P (x, z)) → (P (x, x) → P P (y, z)))φ0 = ¬(∃x∀y(∀z(P (y, z) → P (x, z)) → (P (x, x) → P P (y, z))))φ01 = ∀x∃y((∀z(¬P (y, z) ∨ P (x, z))) & P (x, x) & ¬P (y, z))φ02 = ∀x∃y∀z((¬P (y, z) ∨ P (x, z)) & P (x, x) & ¬P (y, z))S = {¬P (y, z) ∨ P (x, z), P (x, x), ¬P (y, z)}D1 = ¬P (y1 , z1 ) ∨ P (x1 , z1 )D2 = P (x2 , x2 )D3 = ¬P (y3 , z3 )D4D1 ,D2={y1 /x2 ,z1 /x2 }D5D4 ,D3={y3 /x31 ,z3 /x32 }P (x31 , x32 )Упражнение 4.4 Данная задача не рассматривалась на семинарах.
Если будет время, ее решение будетдобавленно. Если пришлете мне решение данной задачи, оно появится тут скорее ;-).185Хорновские логические программы. Декларативные и операционные семантики.Упражнение 5.11. parent(X, Y ) ← f ather(X, Y ).parent(X, Y ) ← mather(X, Y ).2. grandf ather(X, Y ) ← f ather(X, Z), parent(Z, Y ).3. to_be_a_f ather(X) ← f ather(X, Z).4. brother(X, Y ) ← parent(Z, X), man(X), parent(Z, Y ), Z 6= Y.5. of f spring(X, Y ) ← parent(Y, X).of f spring(X, Y ) ← parent(Z, X), of f spring(X, Z).Упражнение 5.21.
list(X)list(nil) ← ;list(X.Y ) ← list(Y ).2. elem(X, Y )elem(X, X.Y ) ← ;elem(X, Z.Y ) ← elem(X, Y );1. T rue.2. X - любой атом.3. F alse.4. X = a, X = b, X = c.5. X - любой списк, содержащий атом a.Упражнение 5.31. list(nil).2. list(A.Y) ← list(Y).1. elem(X, X.Y).2. elem(X, Z.Y) ← elem(X, Y).191. ? list(a.b.c.nil)? list (a.b.c.nil)(2)b.c.n, Y/(1)a{A/il}? list (b.c.nil)(2)l}c.ni, Y/(1)a{A/? list (c.nil)(2)(1)a, Y{A/l}/ni? list (nil)20(2)(1)2. ? list(a.X.nil)? list (a.X1 .nil)(2)Y /X(1)a,{A/nil}1.? list (X2 .nil)(2)(1)il}Y /nX 2,{A/? list (nil)X=A21(2)(1)3.
? list(a.b)? list (a.b)(2)(1)a, Y{A//b}? list (b)22(2)(1)4. ? elem(X, a.b.c.nil)? elem(X1 , a.b.c.nil){Xc/b.1 /aY/a,,X/a,Y/b.,Z/X 1{Xc.nil}(2)l}(1).ni? elem(X2 , b.c.nil)(2)il}(1)c.nY/{X/b,2 /b,X/b,Y/,Z/X 2{Xc.nil}? elem(X3 , c.nil)}(1)nilY/{X/c,3 /a,X/a,,Z/X 3{XY/c.n(2)il }? elem(X4 , nil)X = a, X = b, X = c23(2)(1)5.
? elem(a,X)? elem(a, X1 )(1)/a},XX2Y/{X2,1 /a.Y ,.X/Z{X 1X/a}(2)? elem(a, X2 )2 /a3,(1)/a},XX3Y/{X.X/Z{X 2.Y ,X/a}(2)...24Упражнение 5.41. R(Y) ← P(Y),Q(Y);2. P(a) ← ;3. P(b) ← ;4. Q(a) ← ;5. Q(f(x)) ← Q(X)? R(Y), P(Z)? R(Y), P(Z)(2){Z/a}(1)? P(Z),P(Y),Q(Y)a}(2){Z? P(Y), Q(Y){Z/a, Y/a}{Z/b, Y/a}25(2, 4){Y /a}/b}? P(Y), Q(Y)(2, 4){Y /a}/a}? P(Y)(1)){Y/Z(3){(2, 4){Y /a}? R(Y)(2,4? P(Y),Q(Y)(2, 4){Y /a}b}(1)? P(Y),Q(Y)(3){Z/b}Z){(2}/a? R(Y)(3){Z/Упражнение 5.5% Subelem (X , [ X | _ ]).elem (X , [ _ | Y ]) : - elem (X , Y ).%1head ([ X | _ ] , X ).%2tail ([ _ | Tail ] , Z ) : - tail ( Tail , Z ).tail ([ _ | B ] , B ).%3prefix ([ Head | Tail_1 ] , [ Head | Tail_2 ]) : - prefix ( Tail_1 , Tail_2 ).prefix (_ , []).%4sublist ( List , Sublist ) : - prefix ( List , Sublist ).sublist ([ _ | Tail ] , Sublist ) : - sublist ( Tail , Sublist ).%5less ([ _ | Tail_1 ] , [ _ | Tail_2 ]) : - less ( Tail_1 , Tail_2 ).less ([] , [ _ | _ ]).%6subset ([] , _ ).subset ([ Head | Tail ] , Y ) : - elem ( Head , Y ) , subset ( Tail , Y ).%7concat (X , [] , X ).concat ([ Head | Tail_1 ] , [ Head | Tail_2 ] , X ) : - concat ( Tail_1 , Tail_2 , X ).%8reverse (X , Y ) : - reverse_loop ([] , X , Y ).reverse_loop ( Rev , [] , Rev ).reverse_loop ( Rev , [ Head | Tail ] , Goal ) : - reverse_loop ([ Head | Rev ] , Tail , Goal ).%9period (X , Y ) : - loop_period (X , Y , Y ).loop_period ([] , [] , _ ).loop_period ( Main , [] , Base ) : - loop_period ( Main , Base , Base ).loop_period ([ Head | Main ] , [ Head | Curr ] , Base ) : - loop_period ( Main , Curr , Base ).26Упражнение 5.6%1main_less ([] , [] , 1).main_less ([] , [ _ ] , _ ).main_less ([ _ | Tail_X ] , [ _ | Tail_Y ] , -1) : - main_less ( Tail_X , Tail_Y , -1).main_less ([ _ | Tail_X ] , [ _ | Tail_Y ] , 1) : - main_less ( Tail_X , Tail_Y , 1).main_less ([ A | Tail_X ] , [ A | Tail_Y ] , 0) : - main_less ( Tail_X , Tail_Y , 0).main_less ([0| Tail_X ] , [1| Tail_Y ] , 0) : - main_less ( Tail_X , Tail_Y , 1).main_less ([1| Tail_X ] , [0| Tail_Y ] , 0) : - main_less ( Tail_X , Tail_Y , -1).less ([0| Tail_X ] , Y ) : - less ( Tail_X , Y ).less (X , [0| Tail_Y ]) : - less (X , Tail_Y ).less ([] , [1| _ ]).less ([1| Tail_X ] , [1| Tail_Y ]) : - main_less ( Tail_X , Tail_Y , 0).%2 Z = X + Ysum (X ,Y , Z ) : - reverse (X , R_X ) , reverse (Y , R_Y ) , reverse (Z , R_Z ) , r_sum ( R_X , R_Y , R_Z , 0).r_sum ([ A | Tail_X ] , [ A | Tail_Y ] , [ B | Tail_Z ] , B ) : - r_sum ( Tail_X , Tail_Y , Tail_Z , A ).r_sum ([ _ | Tail_X ] , [ _ | Tail_Y ] , [1| Tail_Z ] , 0) : - r_sum ( Tail_X , Tail_Y , Tail_Z , 0).r_sum ([ _ | Tail_X ] , [ _ | Tail_Y ] , [0| Tail_Z ] , 1) : - r_sum ( Tail_X , Tail_Y , Tail_Z , 1).r_sum ([] , [1| Tail_Y ] , [0| Tail_Z ] , 1) : - r_sum ([] , Tail_Y , Tail_Z , 1).r_sum ([] , [0| Tail_Y ] , [1| Tail_Z ] , 1) : - r_sum ([] , Tail_Y , Tail_Z , 0).r_sum ([1| Tail_X ] , [] , [0| Tail_Z ] , 1) : - r_sum ( Tail_X , [] , Tail_Z , 1).r_sum ([0| Tail_X ] , [] , [1| Tail_Z ] , 1) : - r_sum ( Tail_X , [] , Tail_Z , 0).r_sum ([] , N , N , 0).r_sum (N , [] , N , 0).276Не решенные задачи1.
2.52. 3.33. 4.428.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
