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

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

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

Курсовой проект

Компьютеры, программирование

Другие курсовые по предмету

Компьютеры, программирование

Сдать работу со 100% гаранией

 

 

 

 

 

 

 

 

 

 

 

 

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

 

 

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 2 3 > >>