Размещено на http://www.allbest.ru

Министерство Образования и Науки РФ ФГОУ ВПО

«Дагестанский Государственный Технический Университет»

Филиал в г. Дербент

Курсовая работа

по дисциплине: «Математическая логика и теория алгоритмов»

на тему: «Аналитическое и формальное доказательство теоремы в ИВ»

Выполнила:

Студентка 2 курса

Факультета ПОВТ и АС

Тагирмирзоева Э.

Проверил:

Ст. преподаватель

Гусейнова Л.А.

Дербент 2012 г.

Аннотация

В данной курсовой работе рассматриваются различные способы доказательства истинности рассуждений (теоремы): прямое, формальное, аналитическое и доказательство от противного. Для этого будут использованы следующие алгоритмы: алгоритм Вонга и алгоритм метода пропозициональной резолюций. Также будет проведен анализ этих алгоритмов, используя количественную меру в виде полной энтропии (алгоритмической меры количества информации по Колмогорову), и в соответствии с ним будет представлена рабочая программа на языке Turbo Pascal. истинность доказательство алгоритм пропозициональный

В курсовой работе используются следующие сокращения:

ИВ - Исчисление Высказываний

ППФ - Правильно Построенная Формула

КНФ - Конъюнктивная нормальная форма

Содержание

Введение

Исходные данные

1. Таблица истинности

2. Аналитическое прямое и формальное доказательство истинности заключения (теоремы)

3. Аналитическое и формальное доказательство истинности заключения (теоремы) от противного

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

5. Содержательный словесный алгоритм и граф - схема алгоритма доказательства методом пропозициональной резолюции

6. Сравнительный анализ формальных алгоритмов доказательства по Вонгу и метода пропорциональной резолюции

Заключение

Разработка программы

1. Приложение 1 (рабочая программа по методу пропозициональной резолюции

2. Результат работы программы

Список литературы

Введение

В данной курсовой работе рассматриваются разделы математической логики и теории алгоритмов, необходимые для освоения общепрофессиональных и специальных дисциплин специальности ПОВТ и АС.

Подробно описаны построения таблицы истинности, прямое и обратное доказательство, построение которого основывается на тринадцати законах, которые так же входят в данную курсовую. А также, достаточно подробно, описываются построения алгоритма Вонга и метода резолюции, проводиться сравнение этих методов на удобство реализации программы, которая входит в данную курсовую.

Исходные данные

Посылки:

Теорема:

Правильно построенная формула (ППФ)

() () () () =

1. Таблица истинности

Для начала определим, что такое высказывание. Что называется простое/сложное высказывания в математической логике. Как и на каком основании определяется истинность/ложность высказываний.

Высказывание - утверждение или повествовательное предложение, о котором можно сказать, что оно истинно или ложно т.е. утверждение должен иметь смысл.

Простое называется высказывание, не содержащее связок.

Сложное называется высказывание, содержащее связки.

И так, в нашем случаи высказывание - сложные. И на основе этих сложных высказываний мы строим таблицу истинности.

Буква «И» означает истинность высказывания

«Л» означает ложность высказывания

Существуют два правило, которые применяются к таблице истинности:

1) Для конъюнкции « » - если хотя бы одно простое высказывание ложно, то полученное сложное высказывание становится ложным

2) Для дизъюнкции « » - если хотя бы одно простое высказывание истинно, то полученное сложное высказывание становится истинным

Таблица истинности (ТИ) должна перечислять все возможные комбинации истинности и ложности сложных высказываний.

ТИ строится из, выше описанных, теорем и посылок

() () () () ()

1. 2. 3. 4. 5. 6. () ()

7. () () () 8. () () () ()

9. () () () () ()

10. () () () () ()

11. () () () () ()

A

B

C

D

E

1

2

3

4

5

6

7

8

9

10

11

1

И

И

И

И

И

Л

Л

Л

Л

Л

Л

Л

Л

Л

Л

Л

Л

Л

Л

Л

И

2

И

И

И

И

Л

Л

Л

Л

Л

И

И

Л

Л

Л

Л

И

И

И

И

И

И

3

И

И

И

Л

И

Л

Л

Л

И

Л

Л

Л

И

Л

Л

Л

И

И

И

И

И

4

И

И

И

Л

Л

Л

Л

Л

И

И

Л

Л

И

Л

Л

Л

И

И

И

И

И

5

И

И

Л

И

И

Л

Л

И

Л

Л

Л

И

Л

Л

И

И

И

И

И

И

И

6

И

И

Л

И

Л

Л

Л

И

Л

И

И

Л

Л

Л

И

И

И

И

И

И

И

7

И

И

Л

Л

И

Л

Л

И

И

Л

Л

И

И

Л

И

И

И

И

И

И

И

8

И

И

Л

Л

Л

Л

Л

И

И

И

Л

Л

И

Л

И

Л

И

И

И

И

И

9

И

Л

И

И

И

Л

И

Л

Л

Л

Л

Л

Л

И

Л

Л

Л

И

И

И

И

10

И

Л

И

И

Л

Л

И

Л

Л

И

И

Л

Л

И

Л

И

И

И

И

И

И

11

И

Л

И

Л

И

Л

И

Л

И

Л

Л

Л

И

И

Л

Л

И

И

И

И

И

12

И

Л

И

Л

Л

Л

И

Л

И

И

Л

Л

И

И

Л

Л

И

И

И

И

И

13

И

Л

Л

И

И

Л

И

И

Л

Л

Л

И

Л

Л

Л

И

И

И

И

И

И

14

И

Л

Л

И

Л

Л

И

И

Л

И

И

Л

Л

Л

Л

И

И

И

И

И

И

15

И

Л

Л

Л

И

Л

И

И

И

Л

Л

И

И

Л

Л

И

И

И

И

И

И

16

И

Л

Л

Л

Л

Л

И

И

И

И

Л

Л

И

Л

Л

Л

И

И

И

И

И

17

Л

И

И

И

И

И

Л

Л

Л

Л

Л

Л

Л

Л

Л

Л

Л

Л

Л

И

И

18

Л

И

И

И

Л

И

Л

Л

Л

И

И

Л

Л

Л

Л

И

И

И

И

И

И

19

Л

И

И

Л

И

И

Л

Л

И

Л

Л

Л

Л

Л

Л

Л

Л

Л

Л

И

И

20

Л

И

И

Л

Л

И

Л

Л

И

И

Л

Л

Л

Л

Л

Л

Л

Л

Л

И

И

21

Л

И

Л

И

И

И

Л

И

Л

Л

Л

И

Л

Л

И

И

И

И

И

И

И

22

Л

И

Л

И

Л

И

Л

И

Л

И

И

Л

Л

Л

И

И

И

И

И

И

И

23

Л

И

Л

Л

И

И

Л

И

И

Л

Л

И

Л

Л

И

И

И

И

И

И

И

24

Л

И

Л

Л

Л

И

Л

И

И

И

Л

Л

Л

Л

И

Л

Л

Л

И

И

И

25

Л

Л

И

И

И

И

И

Л

Л

Л

Л

Л

Л

И

Л

Л

Л

И

И

И

И

26

Л

Л

И

И

Л

И

И

Л

Л

И

И

Л

Л

И

Л

И

И

И

И

И

И

27

Л

Л

И

Л

И

И

И

Л

И

Л

Л

Л

Л

И

Л

Л

Л

И

И

И

И

28

Л

Л

И

Л

Л

И

И

Л

И

И

Л

Л

Л

И

Л

Л

Л

И

И

И

И

29

Л

Л

Л

И

И

И

И

И

Л

Л

Л

И

Л

Л

Л

И

И

И

И

И

И

30

Л

Л

Л

И

Л

И

И

И

Л

И

И

Л

Л

Л

Л

И

И

И

И

И

И

31

Л

Л

Л

Л

И

И

И

И

И

Л

Л

И

Л

Л

Л

И

И

И

И

И

И

32

Л

Л

Л

Л

Л

И

И

И

И

И

Л

Л

Л

Л

Л

Л

Л

Л

Л

И

И

Когда конечный результат при любом наборе «Истинно» формула называется общезначимой.

2. Аналитическое прямое и формальное доказательство истинности заключения (теоремы)

В основе прямого доказательства истинности теоремы Q лежит первая версия теоремы дедукции, которая гласит:

- формула Q (теорема, предложение) истинна тогда и только тогда, когда формула

P₁ P₂ … P_n Q

общезначима (т.е. тождественно истинна)

где P₁, P₂, …, P_n - формулы посылок

Q - формула теоремы

На основе этой теоремы докажем истинность следующей формулы с помощью законов логики высказываний:

[()()() ()]

[() () () ()()]

[() () () ()()]

[() () () ()()]=

= () () () () ()=

= ()()()C =

= ()()C = C = `истина'

Представим формальное доказательство теоремы по Вонгу

[()()() ()]

Приведем к КНФ

Все строки доказаны. Следовательно, теорема доказана.

() () () ()()

(), (), (),(), ()

3. Аналитическое и формальное доказательство истинности заключения (теоремы) от противного

В основе доказательства теоремы от противного лежит вторая версия (следствие) теоремы дедукции, которая гласит:

формула Q (теорема, предположение) истинна тогда и только тогда, когда формула

P₁ P₂ … P_n

противоречива. Действительно, если Q - истинна, то формула отрицания Q (т.е. ) ложна, следовательно, из свойства конъюнкции вытекает, что формула противоречива.

Таким образом, для доказательства теоремы от противного, надо осуществлять поиск противоречия в формуле.

Алгоритм поиска противоречия построен на методе пропозициональной резолюции, в основе которого лежит принцип силлогизма.

Сущность, принципа силлогизма состоит в том, что из двух предложений вида (A B) и (A C) следует третье истинное предложение (B C) или

[(A B) (A C)] (B C)

т.е. эта формула является общезначимой (тавтологией).

[()()() ()] () =

= [() () () ()()] () =

= [() () () ()()] () =

= () () () ()() =

= ()()() =

= = `ложь'

Мы получили противоречие, следовательно, теорема доказана.

Представим формальное доказательство теоремы методом резолюции:

[()()() ()] ()

Приведем к КНФ

() () () ()()

Заменив запятой, получим множество ППФ (дизъюнктов)

(), (), (), (), (),

Граф - дерево доказательства от противного.

A

D

E

C

_

C

Мы получили противоречие, следовательно, теорема доказана.

4. Содержательный словесный алгоритм и граф - схема алгоритма доказательства по Вонгу (к п. 1)

(VH) Начало

(V₁) 1. Ввести формулы посылок и теорему

(Z₁) 2. Проверить формулы посылок и теорему на наличие знака эквиваленции, если есть, то перейти к п.3, иначе к п.4.

(V₂) 3. Заменить формулу AB на .

(Z₂) 4. Проверить формулы посылок и теорему на наличие знака импликации, если есть, то перейти к п.5, иначе к п.6.

(V₃) 5. Заменить формулу AB на .

(Z₃) 6. Проверить формулы посылок и теорему на наличие общего отрицания, связывающее две или более букв, если есть, то перейти к п.7, иначе к п.8.

(V₄) 7. Заменить на и на .

(Z₄) 8. Проверить формулы посылок и теорему на наличие двойного отрицания, если есть, то перейти к п.9, иначе к п.10.

(V₅) 9. Заменить на .

(Z₅) 10. Проверить формулы посылок и теорему на наличие дистрибутивности относительно , если есть, то перейти к п.11, иначе к п.12.

(V₆) 11. Заменить формулы на .

(V₇) 12. Выписать формулы посылок слева от стрелки, теорему справа.

(V₈) 13. Заменить слева и справа на запятую.

(Z₆) 14. Проверить есть ли одинаковые и несвязанные высказывательные переменные без отрицания, или с отрицанием, слева или справа от стрелки, если есть, то перейти к п.15, иначе к п.16.

(V₉) 15. Все одинаковые переменные слева и справа от стрелки вычеркнуть.

(Z₇) 16. Проверить есть ли две одинаковые и несвязанные высказывательные переменные без отрицания, или с отрицанием, слева или справа от стрелки, если есть, то перейти к п.17, иначе к п.18.

(V₁₀) 17. Высказывательную переменную с отрицанием перенести слева на права или справа на лево от стрелки с исключением знака отрицания. Пометить что эта строка закрыта (доказана).

(Z₈) 18. Проверить все ли формулы посылок раскрыты, если нет, то перейти к п.19, иначе к п.20.

(Z₉) 19. Проверить все ли переменные несвязны, и одна переменная слева и справа от стрелки в одинаковой форме, если да то перейти к п.20, иначе к п.21.

(V₁₁) 20. Выдать решение. Теорема доказана.

(V₁₂) 21. Разбить i - ю посылку на строки, по каждой высказывательной переменной, перейти к п.14.

(Z₁₀) 22. Проверить все ли высказывательные переменные несвязны и разные.

Если да, то перейти к п. 23 иначе к п. 21.

(V₁₃) 23. Вывести решение. Теорема не доказуема и предположение не верно.

(V_К) Конец

5. Содержательный словесный алгоритм и граф - схема алгоритма доказательства методом пропозициональной резолюции (к п. 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к) Конец.

6. Сравнительный анализ формальных алгоритмов доказательства по Вонгу и метода пропозициональной резолюции

Для сравнительной оценки логической сложности алгоритмов предлагается использовать количественную меру в виде полной энтропии (алгоритмической меры количества информации по Колмогорову) двоичной последовательности

I_A(k, s) = n*H (k, s) (1)

где H (k, s) = - ( log + log + + log ) (2)

или H (k, s) = - ( log + 2 * log ) (3)

n - общее число входов безусловных и условных операторов содержательного алгоритма (граф - схема)

k - число входов безусловных операторов

s₁ - число “единичных” выходов условных операторов

s₀ - число “нулевых” выходов условных операторов

s - число условных операторов (s = s₁ = s₀)

В формуле (1) I_K(k, s) = - n ( log ), бит - доля логической сложности алгоритма по безусловным операторам

I_S(k, s) = - n (2 * log ), бит - доля логической сложности алгоритма по условным операторам.

Формула (1) представляет собой абсолютную логическую сложность алгоритма, измеренную в двоичных единицах (битах).

Для сравнительной оценки сложности двух альтернативных алгоритмов можно использовать формулу = (4)

где I (k, s) I (k, s).

Численное значение позволяет принять решение о выборе алгоритма для реализации программы:

алгоритм, характеризующийся меньшим значением полной энтропии I (k, s) принимается для написания рабочей программы.

Проведем сравнительный анализ алгоритмов доказательства по Вонгу и метода пропозициональной резолюции

	k	s	n
Метод Вонга	13	10	23
Метод резолюции	11	8	19

Найдем полную энтропию для метода Вонга:

1. H (k, s) = - ( log + 2 * log ) 0,4546

2. I_A(k, s) = 23 * 0.4546= 10.4558

Найдем полную энтропию для метода пропозициональной резолюции:

1. H (k, s) = - ( log + 2 * log ) 0,4538

2. I_A(k, s) = 19 * 0.4538= 8,6222

Так как 8,6222 < 10,4558, алгоритм метода пропозициональной резолюции является наиболее эффективным.

Заключение

В данной курсовой работе были рассмотрены различные методы доказательств теорем исчисления высказываний, это аналитические (прямое доказательство истинности теорем и доказательство истинности теорем от противного) и формальные (доказательство теорем методом Вонга и доказательство теорем методом пропозициональной резолюции). К каждому из методов давались словесные (содержательные) алгоритмы, блок-схема, по алгоритму, а также был проведен сравнительный анализ обоих методов. При разработке рабочей программы я столкнулась с проблемой выбора алгоритма, т.к. необходимо было выбрать наиболее эффективный из двух алгоритмов (алгоритм Вонга или алгоритм метода пропозициональной резолюции). Но, проведя сравнительный анализ алгоритмов, я пришла к выводу, что, наиболее эффективным методом для написания программы является метод резолюции.

Для метода пропозициональной резолюции приводится программа и результат выполнения программы для курсового задания.

В ходе выполнения курсовой работы я получила практический опыт и изучила алгоритмы, которые я смогу использовать при решении задач более широкого класса.

Разработка программы

В программе (см. прил. 1) реализующей алгоритм доказательства истинности теоремы методом резолюции используются:

s, s1, s2, s3, news, p, t, pt - переменные типа строка, необходимые для работы со строками.

ekvivalentcia - функция, предназначенная для исключения эквиваленции.

implikacia- функция, предназначенная для исключения импликации

otricanie - функция предназначенная для использования закона Де-Моргана.

dotricanie - функция, предназначенная для использования закона двойного отрицания.

distribut - функция, реализующая применение дистрибутивного закона.

Skobki - функция, предназначенная для удаления лишних скобок.

MetRez - процедура, осуществляющая окончательную проверку строк и вывод результата на экран.

a, b, c, i, j, k, l, m, n, n1, n2 - переменные целого типа.

1. Приложение 1

(рабочая программа по методу пропозициональной резолюции)

Program MR;

Uses crt;

Var t1,p1,pt,p,t:string;

a,b,k,n,i,j,g,l:integer;

{**************************************}

Function ekvivalentcia(s:string):string;

Var a,b,c,k,n,m,i,j:integer;

s1,s2,sa,sb:string;

Begin

s1:=''; k:=0; s2:=s;

For i:= 1 to length(s)do begin

s1:='';

if (s[i]='<') and (s[i+1]='>') then begin

for n:= i downto 1 do if s[n]='(' then break;

for m:= i to length(s) do if s[m]=')' then break;

sa:='';sb:='';

a:=n+1;

While a <> i do begin

sa:=sa+s[a];

a:=a+1;

end;

b:=i+2;

While b<>m do begin

sb:=sb+s[b];

b:=b+1;

end;

s1:='(-(' + sa + ')'+'+('+sb+'))*(-('+sb+')+('+sa+'))';

c:=0;

for j:=1 to length(s2) do begin

if (s2[j]='<') and (s2[j+1]='>') then begin

for n:= j downto 1 do if s2[n]='(' then break;

for m:= j to length(s2) do if s2[m]=')' then break;

delete(s2,n,m-n+1);

insert (s1,s2,n);

c:=c+1;

end;

if c=1 then break;

end;

end;

end;

ekvivalentcia:=s2;

End;

{**************************************}

Function implikacia(s:string):string;

Var a,b,c,k,n,m,i,j:integer;

s1,s2,sa,sb:string;

Begin

s1:=''; k:=0; s2:=s;

For i:= 1 to length(s)do begin

s1:='';

if s[i]='>' then begin

for n:= i downto 1 do if s[n]='(' then break;

for m:= i to length(s) do if s[m]=')' then break;

sa:='';sb:='';

a:=n+1;

While a <> i do begin

sa:=sa+s[a];

a:=a+1;

end;

b:=i+1;

While b<>m do begin

sb:=sb+s[b];

b:=b+1;

end;

s1:='(-'+ '('+sa + ')+'+ '('+sb + '))';

c:=0;

for j:=1 to length(s2) do begin

if s2[j]='>' then begin

for n:= j downto 1 do if s2[n]='(' then break;

for m:= j to length(s2) do if s2[m]=')' then break;

delete(s2,n,m-n+1);

insert (s1,s2,n);

c:=c+1;

end;

if c=1 then break;

end;

end;

end;

implikacia:=s2;

End;

{**************************************}

Function otricanie(s:string):string;

Var k,l,m,n,i,j:integer;

s1,s2:string;

Begin

s1:='';s2:=s;

k:=0;

for i:= 1 to length(s) do

if (s[i]='-') and (s[i+1]='(') then begin

for j:= i+1 to length(s) do if s[j]=')' then break;

for l:= i+1 to j do begin

if (s [l] in ['a'..'z']) or (s[l] in ['A'..'Z'] )then s1:=s1+'-'+s[l]

else if s[l]='+' then s1:=s1+'*'

else if s[l]='*' then s1:=s1+'+'

else s1:=s1+s[l];

end;

k:=0;

n:=pos('-(',s2);

for m:= n+1 to length(s2) do begin

k:=k+1; if s2[m]=')' then break;

end;

delete(s2,n,k+1);

insert(s1,s2,n);

end;

otricanie:=s2;

End;

{**************************************}

Function dotricanie(s:string):string;

Var i:integer;

Begin

for i:= 1 to length(s) do

if (s[i]='-') and (s[i+1]='-') then delete (s,i,2);

dotricanie:=s;

End;

{**************************************}

Function distribut(s:string):string;

Var i,j,g,k,l,r:integer;

a,b,c,s1,s2,st,sp:string;

Begin

s1:=''; a:='';b:='';c:='';

s2:=s; k:=0;

For i:= 1 to length(s) do

if s[i]='(' then begin

for j:= length(s) downto i+1 do if s[j]=')' then g:=j ;

if s[i-1]='+' then

for j:= i to g do if s[j]='*' then k:=k+1;

if k<>0 then

if (s[i-2]='-') or(s[i-2] in ['a'..'z']) or (s[i-2] in ['A'..'Z']) then begin

r:=0; k:=0;sp:='';s1:='';st:='';sp:='';

if (s[i-2] in ['a'..'z'])or (s[i-2] in ['A'..'Z']) then

if s[i-3]='-'then c:='-'+s[i-2] else c:=s[i-2];

for j:=i+1 to g-1 do begin

st:=st+ s[j];r:=r+1;

if (s[j]<>'*') then sp:=sp+s[j];

if (s[j]='*') or (j=g-1) then begin

s1:=s1+'('+c+'+'+sp+')*';sp:='';

end;

end;

delete(s1,length(s1),1);

for j:= 1 to length(s2) do

if pos(st,s2) <>0 then begin

if s[i-3]='-' then begin

delete(s2,i-3,r+5); insert(s1,s2,i-3);

end;

if s[i-3]<>'-' then begin

delete(s2,i-2,r+4); insert(s1,s2,i-2);

end;

end;

end;

if s[g+1]='+' then

for j:= i to g do if s[j]='*' then k:=k+1;

if k<>0 then

if (s[g+2]='-') or(s[g+2] in ['a'..'z']) or (s[g+2] in ['A'..'Z'])then begin

r:=0; k:=0;sp:='';s1:='';st:='';sp:='';

if s[g+2]='-'then c:='-'+s[g+3] else c:=s[g+2];

for j:=i+1 to g-1 do begin

st:=st+ s[j];r:=r+1;

if (s[j]<>'*') and (j<>i+1) then sp:=sp+s[j];

if (s[j]='*') or (j=g-1)then begin

s1:=s1+'(('+c+'+'+sp+')*';sp:='';

end;

end;

delete(s1,length(s1),1);

for j:= 1 to length(s2) do

if pos(st,s2) <>0 then begin

if s[g+2]='-' then begin

delete(s2,i,r+5); insert(s1,s2,i);

end;

if s[g+2]<>'-' then begin

delete(s2,i,r+4); insert(s1,s2,i);

end;

end;

end;

end;

distribut:=s2;

End;

{**************************************}

Function Skobki(s:string):string;

Var a,b,c,k,i,j,g:integer;

Begin

k:=0;

for i:= 1 to length(s) do

if (s[i] in ['a'..'z']) or (s[i] in ['A'..'Z']) then begin

for a:= i downto 1 do if s[a]='(' then break;

for b:= i to length(s) do if s[b]=')' then break;

for c:= a to b do

if (s[c] in ['a'..'z']) or (s[c] in ['A'..'Z']) then k:=k+1;

if k=1 then begin

delete(s,a,1);

delete(s,b-1,1);

end;

k:=0;

end;

Skobki:=s;

End;

{**************************************}

Procedure MetRez(s:string);

Var i,j,g,l,m,n1,n2,poz:integer;

news,s1,s2,s3:string;

Begin

s:=','+s+',';news:=s;

For i:=1 to length(s) do

If s[i]=',' then begin

If i=length(s) then writeln('False');

If i<>length(s) then begin

j:=i+1; s1:='';

While s[j]<>',' do begin

s1:=s1+s[j];

j:=j+1;

end;

l:=j;

While l<>length(news) do begin

If news[l]=',' then begin

g:=l+1;s2:='';

While news[g]<>',' do begin

s2:=s2+news[g];

g:=g+1;

end;

for m:=1 to length(s1) do begin

poz:= pos (s1[m],s2);

if poz <> 0 then

if (s1[m-1]='-') or (s2[poz-1]='-')then begin

s3:='';

for n1:=1 to length(s1) do

if (s1[n1] in ['a'..'z']) or (s1[n1] in ['A'..'Z']) then

if s1[n1]<>s1[m] then

if s1[n1-1]='-' then s3:=s3+'-'+s1[n1]+'+' else s3:=s3+s1[n1];

for n2:=1 to length(s2) do

if (s2[n2] in ['a'..'z']) or (s2[n2] in ['A'..'Z']) then

if s2[n2]<>s1[m] then

if s2[n2-1]='-' then s3:=s3+'-'+s2[n2]+'+' else s3:=s3+s2[n2];

If length(s3)=0 then begin

writeln('Tru');

l:=length(news)-1;

i:= length(s);

end;

If length(s3)<>0 then begin

s1:=s3;

news:=news +s3+',';

end;

break;

end;

end;

end;

l:=l+1;

end;

end;

end;

End;

{**************************************}

BEGIN

Clrscr;

p:='';p1:='';t:='';

Writeln('- otr-nie');

Writeln('* kon-cia');

Writeln('+ diz-cia');

Writeln('> imp-cia');

Writeln('<> ekv-cia');

Write ('Vvedite kol-vo posilok ');

Readln (n);

for i:= 1 to n do begin

Write('vvedite ', i,' posilky ');

Readln(p1);

if i<>n then p:=p+'('+p1+')'+'*' else p:=p+'('+p1+')';

end;

Write ('Vvedite teoremu ');

Readln (t1);

t:='('+t1+')';

If pos('<>',p)<>0 then begin

p:=ekvivalentcia(p);p:=skobki(p);

end;

If pos('<>',t)<>0 then begin

t:=ekvivalentcia(t);t:=skobki(t);

end;

If pos('>',p)<>0 then begin

p:=implikacia(p); p:=skobki(p);

end;

If pos('>',t)<>0 then begin

t:=implikacia(t);t:=skobki(t);

end;

if pos('-(',p)<>0 then p:=otricanie(p);

if pos('-(',t)<>0 then t:=otricanie(t);

if pos('--',p)<>0 then p:=dotricanie(p);

if pos('--',t)<>0 then t:=dotricanie(t);

p:=distribut(p);

t:=distribut(t);

t:='-('+t+')';

t:= otricanie(t); if pos('--',t)<>0 then t:=dotricanie(t);

delete(t,1,1);delete(t,length(t),1);

pt:=p+'*'+t;

Writeln ('KNF: ',pt);

for i:= 1 to length(pt) do begin

if (pt[i]='+') and (pt[i-1]=')') then delete (pt,i-1,1);

if (pt[i]='*') then pt[i]:=',';

end;

t1:=pt;

for i:= 1 to length(t1) do

if (t1[i] ='(') or (t1[i]=')') then begin

j:=pos(t1[i],pt);

delete(pt,j,1);

end;

Writeln('PPF: ',pt);

MetRez(pt);

END.

2.Результат выполнения программы.

Список литературы

1. Гусейнова Л.А. Курс лекций по дисциплине «МЛиТА». 2012 г.

2. Гаджиев А.А. Методические указания к выполнению лабораторного практикума по дисциплине “Математическая логика и теория алгоритмов” (для специальностей 22.01 - ВМКСиС и ПОВТиАС). Махачкала, 2003 г.

Размещено на Allbest.ru

...