Аналитическое и формальное доказательство теоремы в ИВ
Курсовой проект - Компьютеры, программирование
Другие курсовые по предмету Компьютеры, программирование
Аналитическое и формальное доказательство теоремы в ИВ
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. Заменить формулу AB на
(Z2) 4. Проверить формулы посылок и теорему на наличие знака импликации, если есть, то перейти к п. 5, иначе к п. 6.
(V3) 5. Заменить формулу AB на
(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. Проверяем все форму?/p>