Аналитическое и формальное доказательство теоремы в ИВ
Аналитическое и
формальное доказательство теоремы в ИВ
1. Аналитическое прямое и формальное
доказательство истинности заключения (теоремы)
истинность вонг алгоритм программа
В основе прямого доказательства истинности теоремы Q лежит первая версия
теоремы дедукции, которая гласит:
формула Q (теорема, предложение) истинна тогда и только тогда, когда
формула
P1 P2 … Pn ® Q
общезначима (т.е. тождественно истинна)
где P1, P2, …, Pn - формулы посылок
Q - формула теоремы
На основе этой теоремы докажем истинность следующей формулы с
помощью законов логики высказываний:
[()()() ()]
[() ()() ()]=
= () () () ()=
=
= ()()D =
= ()D =
CD=
=
= ‘истина’
Представим формальное доказательство теоремы по Вонгу
[() () () ()]
Приведем к КНФ
()()() () .
2. Аналитическое и формальное доказательство истинности заключения
(теоремы) от противного
В основе доказательства теоремы от противного лежит вторая
версия (следствие) теоремы дедукции, которая гласит:
формула Q (теорема, предположение) истинна тогда и только тогда, когда
формула
P1 Ù P2 Ù … Ù Pn Ù
противоречива. Действительно, если Q - истинна, то формула отрицания Q (т.е. ) ложна, следовательно, из свойства
конъюнкции вытекает, что формула противоречива.
Таким образом, для доказательства теоремы от противного, радо
осуществлять поиск противоречия в формуле.
Алгоритм поиска противоречия построен на методе пропозициональной
резолюции, в основе которого лежит принцип силлогизма.
Сущность, принципа силлогизма состоит в том, что из двух
предложений вида (A Ú B) и (ùA Ú C) следует третье истинное предложение (B Ú C) или
[(A Ú B) Ù
(ùA Ú C)] ® (B Ú C)
т.е. эта формула является общезначимой (тавтологией).
() () () () = =
= [() () () ()] () =
= () () () () =
= () () () =
= B()C() =
= BDC =
BDC B= ‘ложь’
Мы получили противоречие, следовательно, теорема доказана.
Представим формальное доказательство теоремы методом
резолюции:
() () () ()
Приведем к КНФ
() () () ()
Заменив Ù запятой, получим множество ППФ
(дизъюнктов)
(), (), (), (),
Граф - дерево доказательства от противного.
Мы получили противоречие, следовательно, теорема доказана.
3. Содержательный словесный алгоритм и граф -
схема алгоритма доказательства по Вонгу (к п. 1)
(VH) Начало
(V1) 1. Ввести формулы посылок и теорему
(Z1) 2. Проверить формулы посылок и теорему на наличие знака
эквиваленции, если есть, то перейти к п. 3, иначе к п. 4.
(V2) 3. Заменить формулу A«B на
(Z2) 4. Проверить формулы посылок и теорему на наличие знака
импликации, если есть, то перейти к п. 5, иначе к п. 6.
(V3) 5. Заменить формулу A®B на
(Z3) 6. Проверить формулы посылок и теорему на наличие общего
отрицания, связывающее две или более букв, если есть, то перейти к п. 7, иначе
к п. 8.
(V4) 7. Заменить на и на .
(Z4) 8. Проверить формулы посылок и теорему на наличие двойного
отрицания, если есть, то перейти к п. 9, иначе к п. 10.
(V5) 9. Заменить на .
(Z5) 10. Проверить формулы посылок и теорему на наличие
дистрибутивности Ú
относительно Ù, если
есть, то перейти к п. 11, иначе к п. 12.
(V6) 11. Заменить формулы на .
(V7) 12. Выписать формулы посылок слева от стрелки, теорему справа.
(V8) 13. Заменить Ù
слева и Ú справа на запятую.
(Z6) 14. Проверить есть ли одинаковые и несвязанные высказывательные
переменные без отрицания, или с отрицанием, слева или справа от стрелки, если
есть, то перейти к п. 15, иначе к п. 16.
(V9) 15. Все одинаковые переменные слева и справа от стрелки
вычеркнуть.
(Z7) 16. Проверить есть ли две одинаковые и несвязанные
высказывательные переменные без отрицания, или с отрицанием, слева или справа
от стрелки, если есть, то перейти к п. 17, иначе к п. 18.
(V10) 17. Высказывательную переменную с отрицанием перенести слева на
права или справа на лево от стрелки с исключением знака отрицания. Пометить что
эта строка закрыта (доказана).
(Z8) 18. Проверить все ли формулы посылок раскрыты, если нет, то
перейти к п. 19, иначе к п. 20.
(Z9) 19. Проверить все ли переменные несвязны, и одна переменная
слева и справа от стрелки в одинаковой форме, если да то перейти к п. 20, иначе
к п. 21.
(V11) 20. Выдать решение. Теорема доказана.
(V12) 21. Разбить i - ю посылку на строки, по каждой высказывательной
переменной, перейти к п. 14.
(Z10) 22. Проверить все ли высказывательные переменные несвязны и
разные.
Если да, то перейти к п. 23 иначе к п. 21.
(V13) 23. Вывести решение. Теорема не доказуема и предположение не
верно.
(VК) Конец
4. Содержательный словесный алгоритм и граф -
схема алгоритма доказательства методом пропозициональной резолюции (к п. 3)
(Vn) Начало
(V1) 1. Вводим формулы посылок и теоремы
(Z1) 2. Проверяем все формулы на наличии эквиваленции,
если есть эквиваленция, то переходим к п. 3, иначе - к п. 4.
(V2) 3. Заменяем эквиваленцию по формуле:
(Z2) 4. Проверяем все формулы на наличии
импликации, если есть импликация, то переходим к п. 5, иначе - к п. 6
(V3) 5. Заменяем импликации дизъюнкциями по
формуле:
(Z3) 6. Проверяем все формулы на наличие
общей инверсии, если есть общая инверсия, то переходим к п. 7, иначе - к п. 8
(V4) 7. Применяем правило де Моргана: ,
(Z4) 8. Проверяем все формулы на наличие
дистрибутивности, если есть дистрибутивность, то переходим к п. V5, иначе к п. V6
(V5) 9. Применяем дистрибутивный закон:
,
(V6) 10. Полученную преобразованную формулу теоремы инвертируем.
(V7) 11. Все полученные предложения (дизъюнкты) помещаются в единую
группу из n
элементов
(V8) 12. Отбираем из группы (полученная выше) по очерёдности, от 1
до n, одно предложение(s1), которое ранее не
бралось
(Z5) 13. Если в группе нет предложений (s1), которые ранее не
брались, то теорема опровергается, и переходим к п. Vk. Иначе к п. V9
(V9) 14. Отбираем из группы второе предложение (s2), такое что оно не
является s1,
и ранее не бралось (после последнего отбора предложения s1)
(Z6) 15. Если в группе нет предложения (s2) которые ранее не
брались, то переходим к пункту V8. Иначе к п. Z7
(Z7) 16. Если в одном из двух предложений
существует такая переменная, что в другом предложении существует переменная, то переходим к п.V10. Иначе к п.V9.
(V10) 17. Из этих двух предложений строится
новое предложение (s3), состоящее из соединенных связкой И
элементов двух отобранных предложений, причём включаются все элементы, кроме и . Предложение s1 заменяется
полученным предложением (s3).
(Z8) 18. Если в результате слияния получили
пустое предложение, то мы получили противоречие, следовательно теорема доказана
и переходим к п. Vk. Иначе к п. V11
(V11) 19. Вновь образованное предложение
включается в группу и переходим к п.V9.
(Vк) Конец.
5. Сравнительный анализ формальных алгоритмов
доказательства по Вонгу и метода пропорциональной резолюции
Для сравнительной оценки логической сложности алгоритмов
предлагается использовать количественную меру в виде полной энтропии
(алгоритмической меры количества информации по Колмагороу) двоичной
последовательности
IA(k, s) = n*H (k, s) (1)
где H
(k, s) = - ( log + log + + log ) (2)
или H
(k, s) = - ( log + 2 * log ) (3) - общее
число входов безусловных и условных операторов
содержательного алгоритма (граф - схема)
k - число входов безусловных операторов
s1 - число
«единичных» выходов условных операторов
s0 - число
«нулевых» выходов условных операторов
s - число условных операторов (s = s1 = s0)
В формуле (1) IK(k, s) = - n ( log ), бит - доля логической сложности
алгоритма по безусловным операторам
IS(k, s) = - n (2 * log ), бит - доля логической сложности
алгоритма по условным операторам.
Формула (1) представляет собой абсолютную логическую
сложность алгоритма, измеренную в двоичных единицах (битах).
Для сравнительной оценки сложности двух альтернативных
алгоритмов можно использовать формулу
a = (4)
где I (k, s) ³ I (k, s).
Численное значение a позволяет принять решение
о выборе алгоритма для реализации программы:
– алгоритм, характеризующийся меньшим значением полной
энтропии I
(k, s) принимается для
написания рабочей программы.
Заключение
В данной курсовой работе были рассмотрены различные методы
доказательств теорем исчисления высказываний, это аналитические (прямое
доказательство истинности теорем и доказательство истинности теорем от
противного) и формальные (доказательство теорем методом Вонга и доказательство
теорем методом пропозициональной резолюции). К каждому из методов давались
словесные (содержательные) алгоритмы, блок-схема, по алгоритму, а также был
проведен сравнительный анализ обоих методов. При разработке рабочей программы я
столкнулся с проблемой выбора алгоритма, т.к. необходимо было выбрать наиболее
эффективный из двух алгоритмов (алгоритм Вонга или алгоритм метода
пропозициональной резолюции). Но, проведя сравнительный анализ алгоритмов, я
пришел к выводу, что, наиболее эффективным методом для написания программы
является метод резолюции.
Для метода пропозициональной резолюции приводится программа и
результаты выполнения программы для курсового задания.
В ходе выполнения курсовой работы я получил практический опыт
и изучил алгоритмы, которые я смогу использовать при решении задач более
широкого класса.
Приложение 1. (рабочая программа по методу
пропозициональной резолюции)
uses crt;mas=array [1.. 50,1..40] of string[2];stp:mas;
sx:array [1..40] of byte;
i, j, n:byte;
{**************************************************************}
{Процедура ввода и преобразования формул}
Procedure Wwod;np, j, i, k, n1, n2:byte;
ss, s1:string;
sc:char;
Procedure Obrab (c1, c2:char);
Procedure zamena;
var i:byte;
begin
i:=pos ('(', s1);
while i<>0 do
begin
s1 [i]:=' (';
i:=pos ('(', s1);
end;
i:=pos(')', s1);
while i<>0 do
begin
s1 [i]:=')';
i:=pos(')', s1);
end;
i:=pos ('-', s1);
while i<>0 do
begin
s1 [i]:='^';
i:=pos ('-', s1);
end;
end;
{**************************************************************}
{Процедура применения закона Де Моргана}
Procedure DeMorgan (var s1:string);
var i, j, k:byte;
begin
i:=pos ('^', s1); delete (s1, i, 2);
k:=pos(')', s1); delete (s1, k, 1);
while true do
begin
if s1 [i]='^' then
begin
delete (s1, i, 1);
inc(i);
dec(k)
end
else
begin
insert ('-', s1, i);
inc (i, 2);
inc(k)
end;
if i=k then break;
if s1 [i]='+' then s1 [i]:='*'
else s1 [i]:='+';
inc(i);
end;
end;
{**************************************************************}
{Процедура применения дистрибутивного
закона}
Procedure Disp;
var i, j, k:byte;
sp:string;
Function dis (s:string):string;
var x, l, i, j, p,
n:byte;
s1, s2, sn:string[80];
begin
i:=pos ('(', s); j:=pos(')', s); sn:='';
if (s [j+1]=c1) and (j<>length(s)) then
begin
x:=i;
s1:=copy (s, i+1, j-i-1);
l:=length(s); p:=l;
for n:=j+2 to l do
if s[n]=c2 then
begin
l:=n;
break
end;
if l=p then s2:=copy (s, j+1, l-j)
else s2:=copy (s, j+1, l-j-1);
if l=p then delete (s, i, l-i+1)
else delete (s, i, l-i);
repeat
i:=pos (c2, s1);
if i=0 then
begin
i:=length(s1);
insert (copy(s1,1, i)+s2+', ', sn, 1);
delete (sn, length(sn), 1);
insert (sn, s, x);
delete (sn, 1,80);
break;
end;
insert (copy(s1,1, i-1)+s2+', ', sn, 1);
delete (s1,1, i)
until false;
end
else
begin
s1:=copy (s, i+1, j-i-1);
l:=1;
for n:=i-2 downto 1 do
if s[n]=c2 then
begin
l:=n;
break
end;
if l=1 then
begin
s2:=copy (s, 1, i-l);
x:=1;
end
else
begin
s2:=copy (s, l+1, i-l-1);
x:=l+1;
end;
if l=1 then delete (s, 1, j)
else delete (s, l+1, j-l);
repeat
i:=pos (c2, s1);
if i=0 then
begin
i:=length(s1);
insert (s2+copy (s1,1, i)+', ', sn, 1);
delete (sn, length(sn), 1);
insert (sn, s, x);
delete (sn, 1,80);
break;
end;
insert (s2+copy (s1,1, i-1)+', ', sn, 1);
delete (s1,1, i);
until false;
end;
dis:=s;
end;
repeat
i:=pos ('(', s1);
j:=pos ('^', s1);
k:=pos(')', s1);
if i=j+1 then
if ((s1 [j-1]=c2) or (s1 [j-1]=', ') or
(j=1)) and
((s1 [k+1]=c2) or (s1 [k+1]=', ') or
(k=length(s1))) then
begin
DeMorgan(s1);
continue;
end;
if (i<>j+1) and (j<i) and (j<>0)
then
begin
s1 [j]:='-';
continue;
end;
if (i=j+1) then
begin
sp:=copy (s1, j, k-i+2);
delete (s1, j, 1);
delete (s1, i, k-i-1);
DeMorgan(sp);
insert (sp, s1, i);
end;
if i>0 then s1:=dis(s1);
until pos ('(', s1)=0;
end;
if pos ('(', s1)>0 then Disp;
zamena;;
{**************************************************************}
{Процедура инверсии формулы (строки) s1}
Procedure inversia;
var i, j, k:byte;
s:string;
Procedure proverka;s:^string;:=pos ('(', s1);
j:=pos(')', s1);
while i<>0 do
begin
s^:=copy (s1, i+1, j-1-i);
if (((i=1) or (s1 [i-1]='+')) and (s1 [i-1]<>'^'))
and((s1 [j+1]='+') or (j=length(s1)))
then
begin
delete (s1, i, 1);
delete (s1, j - 1,1)
end
else
if (pos ('+', s^)=0) and((((i=1) or
(s1 [i-1]='*')) and
(s1 [i-1]<>'^'))
and((s1 [j+1]='*') or (j=length(s1)))) then
begin
delete (s1, i, 1);
delete (s1, j - 1,1)
end
else
begin
s1 [j]:=')';
s1 [i]:=' (';
end;
i:=pos ('(', s1); j:=pos(')', s1);
end;;:=pos ('(', s1); j:=0;i<>0 do
begin
if (i=1) or (s1 [i-1]<>'^') then
begin
insert ('^', s1, i);
inc(i)
end
else
begin
delete (s1, i - 1,1);
dec(i)
end;:=pos(')', s1);
s1 [i]:=' ['; s1 [k]:=']';
i:=pos ('(', s1);
end;:=s1;
i:=pos ('(', s);
if (i=1) or (i=2) then
begin
k:=pos(')', s);
j:=j+k+1;
if j-1<length(s1)
then
begin
if s1 [j]='*' then s1 [j]:='+'
else s1 [j]:='*'
end;
delete (s, 1, k+1);
end
else
begin
if s[1]='^' then
begin
delete (s1, j+1,1);
delete (s, 1,3);
if j<length(s1) then
begin
if s1 [j]='+' then s1 [j]:='*'
else s1 [j]:='+'
end;
end
else
begin
insert ('^', s1, j+1);
inc (j, 3);
if j<length(s1) then
begin
if s1 [j]='+' then s1 [j]:='*'
else s1 [j]:='+'
end;
delete (s, 1,2);
end
endlength(s)=0;
proverka;;
{**************************************************************}
{Процедура исключения импликации путём замены на
эквивалентную формулу в строке s1}
Procedure implik;i, j, k:byte;pos ('>', s1)<>0
do
begin
i:=pos ('>', s1);
if s1 [i-1]=')' then
begin
j:=pos(')', s1);
while j<>i-1 do
begin
k:=pos ('(', s1);
s1 [j]:=']'; s1 [k]:=' [';
j:=pos(')', s1);
end;
k:=pos ('(', s1);
insert ('^', s1, k);
s1 [i+1]:='+';
end
else
begin
insert ('^', s1, i-1);
s1 [i+1]:='+';
end;
end;;
{**************************************************************}
{Процедура исключения двойного отрицания из
строки s1}
Procedure inverX2;i:byte;pos ('^', s1)<>0 do
begin
i:=pos ('^', s1);
if s1 [i+1]='^' then delete (s1, i, 2)
else s1 [i]:='-';
end;pos ('-', s1)>0 do
begin
i:=pos ('-', s1);
s1 [i]:='^';
end;;
{**************************************************************}
{Процедура исключения эквиваленции путём замены на
эквивалентную формулу в строке s1}
Procedure ekvivalentia;i, j, k:byte;
s2, s3:string[2];
ss:string[20];
i:=pos ('<', s1);
if (s1 [i-2]='^') and (i-1<>1)
then
begin
s2:=copy (s1, i - 2,2);
j:=i-2
end
else
begin
s2:=copy (s1, i - 1,1);
j:=i-1
end;
if (s1 [i+2]='^') and (i+1<>length(s1))
then
begin
s3:=copy (s1, i+2,2);
k:=i+4-j
end
else
begin
k:=i+3-j;
s3:=copy (s1, i+2,1);
end;
delete (s1, j, k);
ss:=' ('+'^'+s2+'+'+s3+')'+'*'+'
('+s2+'+'+'^'+s3+')';
insert (ss, s1, j);pos ('<>', s1)=0;
end;
;(' Введите количество посылок:');
readln(np);;:=0;i:=1 to np do
begin
write ('введите', i, '-ю строку:');
readln(s1);
if pos ('<>', s1)<>0 then ekvivalentia;
if pos ('>', s1)<>0 then implik;
inverX2;
Obrab ('+', '*');
j:=pos ('*', s1);
while j<>0 do
begin
s1 [j]:=', ';
j:=pos ('*', s1);
end;
repeat
n1:=1;
inc(n);
k:=pos (', ', s1);
if k=0 then k:=length(s1)+1;
ss:=copy (s1,1, k-1);
delete (s1,1, k);
repeat
n2:=pos ('+', ss);
if n2=0 then n2:=length(ss)+1;
stp [n, n1]:=copy (ss, 1, n2-1);
delete (ss, 1, n2); inc(n1);
until length(ss)=0;
sx[n]:=n1-1;
until length(s1)=0;
end;
write ('введите теорему:'); readln(s1);
if pos ('<>', s1)<>0 then ekvivalentia;
if pos ('>', s1)<>0 then implik;
Obrab ('+', '*');
inverX2;
inversia;
inverX2;
i:=pos ('*', s1);
while i<>0 do
begin
s1 [i]:=', ';
i:=pos ('*', s1);
end;
repeat
n1:=1;
inc(n);
k:=pos (', ', s1);
if k=0 then k:=length(s1)+1;
ss:=copy (s1,1, k-1);
delete (s1,1, k);
repeat
n2:=pos ('+', ss);
if n2=0 then n2:=length(ss)+1;
stp [n, n1]:=copy (ss, 1, n2-1);
delete (ss, 1, n2);
inc(n1);
until length(ss)=0;
sx[n]:=n1-1;
until length(s1)=0;;
{**************************************************************}
{Процедура применения метода пропозициональной резолюции к
группе формул
(массива)}
Procedure MetRezolut (var a:mas);cop (var
sw:string; ss:string);:='';length(ss)<>0 do
begin
if ss[1]='^' then
begin
sw:=sw+copy (ss, 1,2)+'+';
delete (ss, 1,2)
end
else
begin
sw:=sw+copy (ss, 1,1)+'+';
delete (ss, 1,1)
end;
end;(sw, length(sw), 1);;b:boolean;
q, i, j, j1, h, k:byte;
x:string[2];
s:string;
f:text;
sj1, sj, si:set of byte;
sw1, sw2, sw3:string;;(f, 'rez.txt');(f); (f,
' введеные строки ');
writeln (f, '***********************');i:=1 to n
do
begin
s:='';
for j:=1 to sx[i] do s:=s+a [i, j]+'+';
delete (s, length(s), 1);
writeln (f, s, ' < - ', i, '-я строка ');
end;(f, '***********************');q:=1 to n do
begin
s:='';
si:=[];
include (si, q);
for j:=1 to sx[q] do s:=s+a [q, j];
sw1:='';
cop (sw1, s);
writeln (f, sw1,' <- исходная строка ');
repeat
b:=false;
for i:=1 to n do
begin
if not (i in si) then
begin
sj:=[];
sw1:='';
cop (sw1, s);
for j:=1 to sx[i] do
begin
x:=a [i, j];
h:=length(x);
if h=2 then
begin
delete (x, 1,1);
dec(h)
end
else
begin
insert ('^', x, 1);
inc(h)
end;
k:=pos (x, s);
if (k>0) and (s[k-1]='^') and (a[i, j]=copy (s, k - 1,2)) then
begin
k:=0;
sj:=sj+[j];
end
else if k>0 then
begin
sj1:=sj1+[j];
delete (s, k, h)
end;
end;
if sj1<>[] then
begin
for j:=1 to sx[i] do
if (not (j in sj1)) and (not (j in sj))
then s:=s+a [i, j];
b:=true;
include (si, i);
sj1:=[];
sw2:='';
for j:=1 to sx[i] do sw2:=sw2+a [i, j];
cop (sw2, sw2);
if length(s)<>0 then cop (sw3, s)
else sw3:='__';
writeln (f, sw3,' выведена из:', sw1,' и ', sw2);
if length(s)=0 then
begin
writeln (f, ’ получили противоречие, значит теорема
доказана ');
writeln (f, '***********************');
close(f);
exit;
end;
break;
end;
end;
if b then break
end;
if (i=n) and (not(b)) then break;
until false;
writeln (f, ''Не возможно построить ни одного нового
предложения ');
end;
writeln (f, ' теорема не доказана, т.к. не возможно
получить противоречия ');
writeln (f, '***********************');
close(f);;
{**************************************************************}i:=1
to 50 doj:=1 to 40 do stp [i, j]:='0';;;(stp);('резульат смотрите в файле rez.txt');.
Результат выполнения программы.
Введите количество посылок: 4
Ведите 1-ю посылку:
Ведите 2-ю посылку:
Ведите 3-ю посылку:
Ведите 4-ю посылку:
Введите теорему:
<<Данная теорема истинна>>
Список литературы
1. Гаджиев
А.А. Курс лекций по дисциплине «МЛиТА». 2004 г.
2. Гаджиев
А.А. Методические указания к выполнению лабораторного практикума по дисциплине
«Математическая логика и теория алгоритмов» (для специальностей 22.01 - ВМКСиС
и ПОВТиАС). Махачкала, 2003 г.