Аналитическое и формальное доказательство теоремы в ИВ
Курсовой проект - Компьютеры, программирование
Другие курсовые по предмету Компьютеры, программирование
»ы на наличие дистрибутивности, если есть дистрибутивность, то переходим к п. 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);<