Mat_Logika_Algebra_i_ischislenie_vyskazyvany

41

строению переменных Bi . Добавим к аксиомам АТЧ аксиому

А4. F(A1,..., An ) .

Выводимость в этом новом исчислении будем обозначать – F .

Так как формула F(B1,...,Bn ) получена по схеме А4, то

1. F F(B1,...,Bn ) (А4).

Возьмем произвольную формулу C. Тогда формула F(B1,...,Bn ) C –

так как ее вывод в новом исчислении тот же, что и в АТЧ. Применяя МР к 1 и 2, получим, что

3. F C (МР к 1 и 2).

Аналогично и для ¬C получим, что F ¬C . Таким образом, в новой теории с добавленной аксиомой одновременно выводимы формула и ее отрицание. Следовательно, расширенная теория противоречива, а значит АТЧ абсолютно непротиворечива. ■

42

ЛИТЕРАТУРА

1.Андерсон Дж.А. Дискретная математика и комбинаторика. М.: Изд. дом

«Вильямс», 2003. – 960 с.

2.Верещагин Н.К., Шень.А. Лекции по математической логике и теории алгоритмов. Часть 2. Языки и исчисления. М.: МЦНПМО, 2002. – 288 с.

3.Гаврилов Г.П., Сапоженко А.А. Задачи и упражнения по дискретной математике. М.: ФИЗМАТЛИТ, 2004. – 416 с.

4.Кузнецов О.П., Адельсон–Вельский Г.М. Дискретная математика для ин-

женера. М.: «Энергия», 1980. – 344 с.

5.Мендельсон Э. Введение в математическую логику. М.: «Наука», 1984. –

478с.

6.Нефедов В.Н., Осипова В.А. Курс дискретной математики. М.: МАИ, 1992,

–576 с.

7.Новиков Ф.А. Дискретная математика для программистов. СПб.: «Питер», 2000. – 304 с.

8.Романовский И.В. Дискретный анализ. СПб.: «Невский диалект», 2000. –

240с.

9.Хаггарти Р. Дискретная математика для программистов. М.: «Техносфера», 2004. – 320 с.

43

ПРИЛОЖЕНИЯ

44

Приложение 1. Контрольные задания для построения таблиц истинности и нормальных форм

В каждом из вариантов следует построить по исходной логической фор-

муле:

1)таблицу истинности;

2)привести исходную логическую формулу с помощью равносильностей к нормальной дизъюнктивной форме (ДНФ);

3)привести исходную логическую формулу с помощью равносильностей к нормальной конъюнктивной форме (КНФ); (необязательно начинать с исходной формулы – можно с уже полученной ДНФ);

4)получить из нормальной дизъюнктивной формы совершенную нормальную дизъюнктивную форму (СДНФ);

5)получить из нормальной конъюнктивной формы совершенную нормальную конъюнктивную форму (СКНФ);

6)по элементарным конъюнкциям СДНФ и элементарным дизъюнкциям СКНФ вывести оценки списка переменных на которых элементарные конъюнкции принимают значение Истина, а элементарные дизъюнкции – значение Ложь. Сравнить эти оценки с таблицей истинности.

45

Варианты заданий

1.((A & ¬B) C ) (A (B & C)).

2.((B & ¬C ) A) (A ¬C).

3.(A & (B A)) (¬(¬B C )).

4.((A & ¬B) B)¬(B C ).

5.(A (B & ¬C )) ((A B) (A C )).

6.(A & (B ¬C )) (¬B A).

7.((B A) ((¬A & B) (A C )))& C .

8.((B A) C) ((A ¬B) (A ¬C )).

9.((¬X Y ) (¬X (Y & Z )))& Z .

10.(A ¬(B & C )) ((¬A C )& B).

11.(X (X &Y )) ((X ¬Z )&Y ).

12.((X Y )& ¬Y ) ((Z ¬X )&Y ).

13.(¬X (Y ¬Z )) ((X ¬Y ) (X ¬Z )).

14.(¬X & (¬Y ¬Z )) ((Y X ) (X & Z )).

15.(¬X Y ) (((¬X & Y ) (X Y ))& Z ).

16.((¬X & ¬Y ) Z ) (X (Y Z )).

17.((X Y )& Z ) (Y Z ).

18.((X &Y ) Z ) (¬Z Y ).

19.(X (Y Z )) ((X &Y ) Z ).

20.((X Y ) Z ) ((¬X Z )¬Y ).

46

21.(A & (B ¬C)) ((B & A) C ).

22.(X (Y & ¬Z )) (X Z ).

23.(X & (Y ¬Z )) ((Y X )& Z ).

24.((X &Y ) Y ) ((¬Y Z )¬X ).

25.(A ¬(B C )) ((¬A B) (A C )).

26.(A & (C B)) ((¬B C ) (A & C )).

27.((A ¬B) ((¬A & ¬B) (A C )))& ¬C .

28.((A B)¬C ) ((A C ) (B ¬C )).

29.((X Y ) ((X Y ) (X & Z )))& Z .

30.((B & C ) A) ((¬A C ) B).

31.(X (X & ¬Y )) (((X Z )& ¬Y ) Y ).

32.((X Y ) ¬Y ) ((X Z ) Y ).

33.(X Y ) (Y (¬X & Z )).

34.(¬X (¬Y ¬Z )) ((X Y ) (X & Z )).

35.(X Y ) (((X &Y ) (¬X Y ))& Z ).

36.((¬X ¬Y ) Z ) ((X Z ) (Y Z )).

37.(X (Y ¬Z )) ((¬Y X ) (X & Z )).

38.(¬X Y ) ((X (Y & Z ))¬Z ).

39.(¬X (¬Y ¬Z )) (Y Z ).

40.((X ¬Y ) (¬X & Z )) (Z (X & Z )).

47

Приложение 2. Программный модуль в математическом пакете «Maple 6» для проверки правильности найденных таблиц истинности и нормальных форм

> restart:

Определение логических связок

> ifthen:=(x,y)->not x or y; # импликация

equiva:=(x,y)->x and y or not x and not y;# эквиваленция

ifthen := ( x, y ) → not x or y

equiva := ( x, y ) → x and y or not ( x or y )

> fDNF:=(x,y,z)->"DNF?";fKNF:=(x,y,z)->"KNF?"; pp:=(x,y,z)->"";

fDNF := ( x, y, z ) → "DNF?" fKNF := ( x, y, z ) → "KNF?" pp := ( x, y, z ) → ""

Процедура создания таблицы истинности логической формулы f от 3-х переменных

и, если заданы логические формулы fDNF и fKNF, то их таблицы истинности,

атакже проверка их равносильности логической формуле f

>GetLog:=proc(f)

local x,y,z,yDNF,yKNF; global fDNF,fKNF; yDNF:=true; yKNF:=true;

printf(" x y %6s %6s %-13s %-13s\n"," z"," f"," ДНФ"," КНФ"):

for x from 1 to 4 do

48

printf("===== "): end do:

printf("%-13s %-13s\n"," ======="," ======="):

for x in false,true do for y in false,true do

for z in false,true do

printf("%-6s %-6s %-6s %-6s %7s%-6s %7s%- 6s\n",x,y,z,f(x,y,z),"ДНФ -> ",fDNF(x,y,z),"КНФ -> ",fKNF(x,y,z)): if(f(x,y,z)<>fDNF(x,y,z)) then yDNF:=false end if:

if(f(x,y,z)<>fKNF(x,y,z)) then yKNF:=false end if: end do

end do end do:

fDNF:=(x,y,z)->"DNF?":fKNF:=(x,y,z)->"KNF?":

if (not yDNF) then print("ДНФ неверная") end if: if (not yKNF) then print("КНФ неверная") end if: end proc;

GetLog := proc (f)

local x, y, z, yDNF, yKNF; global fDNF, fKNF;

yDNF := true; yKNF := true;

printf( " x y %6s %6s %-13s %-13s

", " z", " f", " ДНФ" , " КНФ" ); for x to 4 do printf( "===== " ) end do ; printf( "%-13s %-13s

", " =======", " =======" );

for x in false, true do for y in false, true do for z in false, true do printf( "%-6s %-6s %-6s %-6s %7s%-6s %7s%-6s

", x, y, z, f( x, y, z ), "ДНФ -> ", fDNF( x, y, z ), "КНФ -> ", fKNF( x, y, z ) );

if f( x, y, z ) ≠ fDNF( x, y, z ) then yDNF := false end if ;

50

for y in true,false do for z in true,false do

for x1 in true,false do print(x,y,z,x1,f(x,y,z,x1))

end do end do

end do end do

end proc;

Get4Log := proc (f) local x, y, z, x1;

for x in true, false do for y in true, false do for z in true, false do

for x1 in true, false do print( x, y, z, x1, f( x, y, z, x1 ) ) end do end do

end do end do

end proc

Процедура создания таблицы истинности логической формулы f от 6-х переменных

> Get6Log:=proc(f) local x,y,z,x1,y1,z1; for x in true,false do

for y in true,false do for z in true,false do

for x1 in true,false do for y1 in true,false do

for z1 in true,false do print(x,y,z,x1,y1,z1,f(x,y,z,x1,y1,z1))

end do