Mat_Logika_Algebra_i_ischislenie_vyskazyvany
.pdf41
строению переменных Bi . Добавим к аксиомам АТЧ аксиому
А4. F(A1,..., An ) .
Выводимость в этом новом исчислении будем обозначать – F .
Так как формула F(B1,...,Bn ) получена по схеме А4, то
1. F F(B1,...,Bn ) (А4).
Возьмем произвольную формулу C. Тогда формула F(B1,...,Bn ) C –
тавтология |
в |
силу |
свойств |
импликации. |
Следовательно, |
|||||
|
|
|
F(B1,...,Bn ) C, а значит, |
|
|
|||||
|
|
|
|
|
||||||
|
|
|
|
|
||||||
|
|
|
2. |
|
|
F(B1,...,Bn ) C (Т. о полноте), |
|
|||
|
|
|
|
|
|
|||||
|
|
|
F |
|
так как ее вывод в новом исчислении тот же, что и в АТЧ. Применяя МР к 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 ;
49
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
> fYY:=(x,y,z)->ifthen(x or y,ifthen(not y or z,x or
z));
fDNF:=(x,y,z)-
>ifthen(ifthen(ifthen(x,y),z),ifthen(y,z));
fKNF:=(x,y,z)-
>ifthen(ifthen(ifthen(ifthen(x,y),z),x),ifthen(z,x));
GetLog(fYY);
fYY := ( x, y, z ) → ifthen( x or y, ifthen( not y or z, x or z ) ) fDNF := ( x, y, z ) → ifthen( ifthen( ifthen( x, y ), z ), ifthen( y, z ) )
fKNF := ( x, y, z ) → ifthen( ifthen( ifthen( ifthen( x, y ), z ), x ), ifthen( z, x ) )
x |
y |
z |
f |
===== |
===== |
===== |
===== |
false |
false |
false |
true |
false |
false |
true |
true |
false |
true |
false |
true |
false |
true |
true |
true |
true |
false |
false |
true |
true |
false |
true |
true |
true |
true |
false |
true |
true |
true |
true |
true |
ДНФ
=======
ДНФ -> true ДНФ -> true ДНФ -> true ДНФ -> true ДНФ -> true ДНФ -> true ДНФ -> true ДНФ -> true
КНФ
=======
КНФ -> true КНФ -> true КНФ -> true КНФ -> true КНФ -> true КНФ -> true КНФ -> true КНФ -> true
Процедура создания таблицы истинности логической формулы f от 4-х переменных
> Get4Log:=proc(f)
local x,y,z,x1;
for x in true,false do
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