Проверка логического следования методом резолюции
Курсовой проект - Компьютеры, программирование
Другие курсовые по предмету Компьютеры, программирование
Введение
В данной курсовой работе будет рассмотрен алгоритм проверки логического следования методом резолюции. Его реализация будет представлена па логическом языке Prolog и на функциональном языке Haskell.
Метод резолюции - метод доказательства теорем в теориях первого порядка, использующий правило вывода, называемое резолюцией.
Резолюция заключается в следующем : если выводимые дизъюнкты P \/ Q и ~P \/ R, где P - атомарная формула, а Q и R обозначают остальные части дизъюнктов (возможно пустые), то выводим и дизъюнкт Q \/ R, называемый резольвентой.
Цель данной курсовой работы заключается в том, что необходимо написать программы на двух языках, реализующие алгоритм проверки логического следования методом резолюции, и закрепить пройденный на лекциях материал.
Для решения поставленной цели необходимо решить следующие задачи:
1)проанализировать поставленную задачу;
2)составить алгоритм, с помощью которого будет решена задача;
)реализовать его на языке Prolog;
)реализовать алгоритм на языке Haskell.
алгоритм проверка логический резолюция
Постановка задачи
Итак, рассмотрим алгоритм проверки логического следования методом резолюции. Для начала необходимо рассмотреть принцип резолюции. Допустим, имеется множество дизъюнктов - D, которые представляют некую формулу F. Формула F противоречива тогда и только тогда, когда противоречиво множество дизъюнктов D. Если во множестве D имеется пустой дизъюнкт, то оно не выполнимо. Если в этом множестве нет пустого дизъюнкта, то проверяется возможность получения пустого дизъюнкта из него. Метод резолюции можно применить к любому множеству дизъюнктов, чтобы проверить их противоречивость.
Литеры L и ~L называются контрарными, а множество {L, ~L} - контрарной парой. Если в дизъюнкте D1 существует литера L1, контрарная литере L2 в дизъюнкте D2, то необходимо удалить литеры L1 и L2 из дизъюнктов D1 и D2 соответственно и построить дизъюнкцию оставшихся дизъюнктов. Получившийся дизъюнкт называется резольвентой.
Резолютивный вывод L из множества дизъюнктов D есть такая конечная последовательность L1, L2, ..., Lk дизъюнктов, в которой каждый Li (i=1, ..., k) или принадлежит D, или является резольвентой дизъюнктов, предшествующих Li и Lk= L. Для невыполнимого множества дизъюнктов в результате последовательного применения правила резолюций получается пустой дизъюнкт. Вывод из множества D пустого дизъюнкта называется опровержением (доказательством невыполнимости) D. Следовательно, задача курсовой работы сводится к тому, чтобы реализовать метод доказательства невыполнимости.
Рисунок 1 - Пример доказательства теоремы методом резолюции
Выбор структуры данных
Для данной темы лучше всего подходит структура - список списков. Тогда выражение вида (A v ~C v B) & (~B v ~A v D) & (~D v C) можно записать так: [[A, ~C, B], [~B, ~A, D], [~D, C]], где квадратные скобки определяют дизъюнкт, запятые в них разделяют литеры дизъюнкта. Данная структура наиболее подходящая для этой задачи, потому что эффективна в реализации функций задачи. Например, перестановка не требует полной реконструкции структуры, необходимо только применение операций удаления, вставки, объединение дизъюнктов с такой структурой реализуется просто, при чем с учетом контрарности.
Конечно, можно использовать и другую структуру такую, как дерево, но это будет сложно и громоздко, так как количество операций зависит от количества дизъюнктов и от количества литеров в них, а представление деревьев с большим количеством ветвей сложно и расход памяти будет намного больше, чем при использовании структуры список списков.
Формулировка алгоритма
Итак, рассмотрим этапы решения задачи.
1.Найти все возможные комбинации дизъюнктов.
Необходимо учитывать, что при проверке логического следования методом резолюции на результат влияет последовательность дизъюнктов. Цель данной работы заключается в поиске той последовательности дизъюнктов, которая в результате образует пустую резольвенту.
2.Произвести объединение дизъюнктов с учетом контрарности.
Необходима такая операция объединения, которая будет учитывать контрарность литеров.
Если вводимая стартовая последовательность (комбинация) дизъюнктов образует пустую резольвенту, то проверка логического следования закончена с положительным результатом.
Недостаток алгоритма: если пустая резольвента найдена, а дизъюнкты были задействованы не все, то операция объединения не прекратит выполнение поиска, а продолжит свою работу. Поэтому необходимо использовать переменную, которая будет сообщать при найденной пустой резольвенте о конце работы алгоритма.
Итак, рассмотрев алгоритм решения задачи, перейдем к его реализации на языке Prolog и на языке Haskell.
Реализация алгоритма на языке Prolog
Для начала необходимо определить отношение между атомами (контрарность). По закону математической логики, можно ввести следующее утверждение: $($X):- X, где символ $ будет являться схематической записью отрицания, так как в некоторых версиях SWI-Prolog, символ ~ зарезервирован.
Итак, рассмотрим функции, с помощью которых будем реализовать алгоритм:
1.Функция perestanovka. Порождает все возможные перестановки
элементов списка.
perestanovka([], []).
perestanovka(Z,[X|K]):- udalit(X,Z,Z1), perestanovka(Z1,K).
Если первый список пуст, то результат пуст (базовый случай). Иначе удаляем голову X из первого списка, делаем пер