Семинарские занятия (Решения задач) (1157996), страница 3

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 3)

φ1 = R(a, b)2. φ2 = R(b, c)3. φ3 = R(b, a)4. φ4 = R(c, d5. ψ2 = ∀xQ(x, x)6. ψ2 = ∀x∀y∀z(Q(x, y)&R(y, z) → Q(x, z))18ЗапросΦ1 = Q(a, d)Система дизъюнктовS = {D1 , D2 , D3 , D4 , D5 , D6 , D7 }D1D2D3D4D5D6D7= R(a, b)= R(b, c)= R(b, a)= R(c, d)= Q(X5 , X5 )= ¬Q(X6 , Y6 ) ∨ ¬R(Y6 , Z6 ) ∨ Q(X6 , Z6 )= ¬Q(a, d)Покажем противоречивость данной системы дизъюнктовD8D7 ,D6=¬Q(a, Y8 ){X6 /a,Z6 /d}D9D8 ,D4=¬Q(a, c){Y8 /c}∨ ¬R(Y8 , d)D10D9 ,D6=¬Q(a, Y10 ){X6 /a,Z6 /c}D11D10 ,D2=¬Q(a, b){Y10 /b}D12D11 ,D6=¬Q(a, Y12 ){X6 /a,Z6 /b}D13D12 ,D1=¬Q(a, a){Y12 /a}D14D13 ,D5={X5 /a}∨ ¬R(Y10 , c)∨ ¬R(Y12 , b)195Хорновские логические программы.

Декларативные и операционные семантики.Упражнение 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 ), X 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).201. ? 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)21(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=A22(2)(1)3. ? list(a.b)? list (a.b)(2)(1)a, Y{A//b}? list (b)23(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 = c24(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)...25Упражнение 5.41. R(Y1 ) ← P(Y1 ),Q(Y1 );2. P(a) ← ;3. P(b) ← ;4. Q(a) ← ;5. Q(f(X5 )) ← Q(X5 )? R(Y), P(Z)? R(Y), P(Z)(1){Y /Y1 }b}(2){Y/{Y 11 /a(3)}? P(Y1 ),Q(Y1 ),P(Z)(2){Z(4)/b}(3){Z/a}? P(Z)? Q(b),P(Z){Z/a, Y/a}{Z/b, Y/a}26(5)(5)(4)? Q(a),P(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 ([] , [ _ | _ ]).less ([ _ | Tail_1 ] , [ _ | Tail_2 ]) : - less ( Tail_1 , Tail_2 ).%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 ).27Упражнение 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).286Встроенные функции и предикатыУпражнение 6.1elem ([ X | _ ] , X ).elem ([ _ | A ] , X ) : - elem (A , X ).not_elem ([] , _ ).not_elem ([ A | Y ] , X ) : - A \= X , not_elem (Y , X ).% make_ordered ( L_1 , L_2 ).% insertinsert_sort ( List , Sorted ): - i_sort ( List ,[] , Sorted ).i_sort ([] , Acc , Acc ).i_sort ([ H | T ] , Acc , Sorted ): - insert (H , Acc , NAcc ) , i_sort (T , NAcc , Sorted ).insert (X ,[ Y | T ] ,[ Y | NT ]): - X >Y , insert (X ,T , NT ).insert (X ,[ Y | T ] ,[X , Y | T ]): - X = < Y .insert (X ,[] ,[ X ]).% bubblebubble_sort ( List , Sorted ): - b_sort ( List ,[] , Sorted ).b_sort ([] , Acc , Acc ).b_sort ([ H | T ] , Acc , Sorted ): - bubble (H ,T , NT , Max ) , b_sort ( NT ,[ Max | Acc ] , Sorted ).bubble (X ,[] ,[] , X ).bubble (X ,[ Y | T ] ,[ Y | NT ] , Max ): -X >Y , bubble (X ,T , NT , Max ).bubble (X ,[ Y | T ] ,[ X | NT ] , Max ): - X = <Y , bubble (Y ,T , NT , Max ).% quickquick_sort ( List , Sorted ): - q_sort ( List ,[] , Sorted ).q_sort ([] , Acc , Acc ).q_sort ([ H | T ] , Acc , Sorted ): pivoting (H ,T , L1 , L2 ) ,q_sort ( L1 , Acc , Sorted1 ) , q_sort ( L2 ,[ H | Sorted1 ] , Sorted ).pivoting (_ ,[] ,[] ,[]).pivoting (H ,[ X | T ] ,[ X | L ] , G ): - X = <H , pivoting (H ,T ,L , G ).pivoting (H ,[ X | T ] ,L ,[ X | G ]): - X >H , pivoting (H ,T ,L , G ).% single ( L_1 , L_2 )single ([] ,[]).single ([ A | X ] , Y ) : - single (X , Y ) , elem (Y , A ).single ([ A | X ] , [ A | Y ]) : - single (X , Y ) , not_elem (Y , A ).% common ( L_1 , L_2 , L_3 )common ([] , X , Y ) : - single (X , Y ).common ([ A | X ] , Z , Y ) : - common (X ,Z , Y ) , elem (Y , A ).common ([ A | X ] , Z , [ A | Y ]) : - common (X ,Z , Y ) , not_elem (Y , A ).% intersect ( L_1 , L_2 , L_3 )intersect ([] , _ ,[]).intersect ([ A | X ] , Z , [ A | Y ]) : - elem (Z , A ) , intersect (X ,Z , Y ).intersect ([ A | X ] , Z , Y ) : - not_elem (Z , A ) , intersect (X ,Z , Y ).29Упражнение 6.2% length (L , X )m_length ([] ,0).m_length ([ _ | L ] , X ) : - m_length (L , Z ) , X is Z + 1.% sum (L , X )sum ([ X ] , X ).sum ([ X | L ] , S ) : - sum (L , Z ) , S is X + Z .a_sum (L , X ) : - acc_sum (L , X , 0).acc_sum ([] , X , X ).acc_sum ([ A | L ] , X , ACC ) : - W is A + ACC , acc_sum (L , X , W ).% mult (L , X , Y )mult ([] , _ , 0).mult ([ X | L ] , X , Y ) : - mult (L , X , Z ) , Y is Z + 1.mult ([ A | L ] , X , Y ) : - A \= X , mult (L , X , Y ).% most_of (L , X )most_of ([ X ] , X ).most_of ([ X | L ] , X ) : - most_of (L , Y ) , mult (L , X , M_X ) , mult (L , Y , M_Y ) , M_X >= M_Y .most_of ([ Z | L ] , X ) : - most_of (L , X ) , mult (L , X , M_X ) , mult ([ Z | L ] , Z , M_Z ) , M_X > M_Z .% i_most_of (L , X ) iterativei_most_of (L , X ) : - msort (L , S_L ) , max_mult ( S_L , CURR , 1 , 0 , X ).max_mult ([ _ ] , M_M , CURR , MAX_MULT , M_M ) : - CURR = < MAX_MULT .max_mult ([ A , A | L ] , M_M , CURR , MAX_COUNT , X ) : - NEW_CURR is CURR + 1 , max_mult ([ A | L ] , M_M ,max_mult ([ A , B | L ] , M_M , CURR , MAX_COUNT , X ) : - A \= B , MAX_COUNT >= CURR , max_mult ([ B | L ] ,max_mult ([ A , B | L ] , M_M , CURR , MAX_COUNT , X ) : - A \= B , MAX_COUNT < CURR , max_mult ([ B | L ] , A% prime (L , X )prime ([2] ,2).prime ([ X | L ] , X ) : - Y is X - 1 , prime (L , Y ) , pr (X , L ).prime (L , X ) : - Y is X - 1 , prime (L , Y ) , antipr (X , L ).pr (_ , []).pr (X , [ Y | L ]) : - gcd (X , Y , 1) , pr (X , L ).antipr (X , [ Y | _ ]) : - gcd (X , Y , Z ) , Z > 1.antipr (X , [ Y | L ]) : - gcd (X , Y , 1) , antipr (X , L ).% gcd (X ,Y , Z )gcd (X ,X , X ).gcd (X ,Y , Z ) : - X > Y , N_X is X - Y , gcd ( N_X , Y , Z ).gcd (X ,Y , Z ) : - X < Y , N_Y is Y - X , gcd (X , N_Y , Z ).307Операторы отсечения и отрицанияУпражнение 7.11.

A(Y1 ) ← B(Y1 ), C(a2 , Y1 );2. A(X2 ) ← D(a1 , X2 ), C(X2 ,Y2 );3. B(U3 ) ← D(U3 , V3 ), !, E(V3 );4. B(V4 ) ← E(a5 );5. E(a2 ) ← ;6. E(a3 ) ← ;7. E(Z7 ) ← ;8. D(U8 , a1 ) ← C(U8 , f (U8 ));9. D(U9 , U9 ) ← ;10. D(X10 , a2 ) ← ;11. C(Z11 , a3 ) ← ;? A(X)Дерево не вмещается. Но там все просто ;=).31Упражнение 7.2elem ([ X | _ ] , X ).elem ([ _ | A ] , X ) : - elem (A , X ).% max (X , Y , Z )max (X , Y , X ) : - X >Y , !.max (_ , Y , Y ).% common ( L1 , L2 , L3 ).common ([] , _ , []).common ([ A | L1 ] , L2 , [ A | L3 ]) : - elem ( L2 , A ) , ! , common ( L1 , L2 , L3 ).common ([ _ | L1 ] , L2 , L3 ) : - common ( L1 , L2 , L3 ).% nonsquare ( L1 , L2 )nonsquare ( L1 , L2 ) : - nonsquare_seq ( L1 , L1 , L2 ).nonsquare_seq ([] , _ , []).nonsquare_seq ([ A | L1 ] , SL1 , L2 ) : - M is A * A , elem ( SL1 , M ) , ! ,nonsquare_seq ( L1 , SL1 , L2 ).nonsquare_seq ([ A | L1 ] , SL1 , [ A | L2 ]) : - nonsquare_seq ( L1 , SL1 , L2 ).Упражнение 7.31.

Характеристики

Список файлов семинаров