Проверка логического следования методом резолюции

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

Введение

В данной курсовой работе будет рассмотрен алгоритм проверки логического следования методом резолюции. Его реализация будет представлена па логическом языке Prolog и на функциональном языке Haskell.

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

Резолюция заключается в следующем : если выводимые дизъюнкты P \/ Q и ~P \/ R, где P - атомарная формула, а Q и R обозначают остальные части дизъюнктов (возможно пустые), то выводим и дизъюнкт Q \/ R, называемый резольвентой.

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

Для решения поставленной цели необходимо решить следующие задачи:

1) проанализировать поставленную задачу;

2) составить алгоритм, с помощью которого будет решена задача;

3) реализовать его на языке Prolog;

4) реализовать алгоритм на языке Haskell.

алгоритм проверка логический резолюция

Постановка задачи

Итак, рассмотрим алгоритм проверки логического следования методом резолюции. Для начала необходимо рассмотреть принцип резолюции. Допустим, имеется множество дизъюнктов - D, которые представляют некую формулу F. Формула F противоречива тогда и только тогда, когда противоречиво множество дизъюнктов D. Если во множестве D имеется пустой дизъюнкт, то оно не выполнимо. Если в этом множестве нет пустого дизъюнкта, то проверяется возможность получения пустого дизъюнкта из него. Метод резолюции можно применить к любому множеству дизъюнктов, чтобы проверить их противоречивость.

Литеры L и ~L называются контрарными, а множество {L, ~L} - контрарной парой. Если в дизъюнкте D₁ существует литера L₁, контрарная литере L₂ в дизъюнкте D₂, то необходимо удалить литеры L₁ и L₂ из дизъюнктов D₁ и D₂ соответственно и построить дизъюнкцию оставшихся дизъюнктов. Получившийся дизъюнкт называется резольвентой.

Резолютивный вывод L из множества дизъюнктов D есть такая конечная последовательность L₁, L₂, ..., L_k дизъюнктов, в которой каждый L_i (i=1, ..., k) или принадлежит D, или является резольвентой дизъюнктов, предшествующих L_i и L_k= 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 из первого списка, делаем перестановку его хвоста - получаем некий список K, затем добавляем X в его начало.

2. Функция udalit. Удаляет элемент из списка.

udalit(X,[X|Xs],Xs).

udalit(X,[Y|Ys],[Y|Z]):- udalit(X,Ys,Z).

Если элемент совпадает с головой второго списка, то результатом будет хвост списка (базовый случай). Иначе результатом будет список голова, которого совпадает с головой исходного списка, а хвост получается удалением заданного элемента из хвоста заданного списка.

3. Функция vhodit. Проверяет принадлежность элемента к списку.

vhodit(X, [X|_]).

vhodit(X,[_|Xs]):- vhodit(X, Xs).

Элемент принадлежит списку, если он сопоставим с головой списка (базовый случай). Иначе элемент принадлежит хвосту второго списка.

4 Функция contrar. Проверяет контрарность литеров. Prolog-машина воспринимает X и $X как два разных выражения, так как $X есть не литер, а результат функции $. Поэтому рассматриваются два случая, которые различаются контрарностью первых элементов.

contrar(X,[$X|_]).

contrar(X,[_|Xs]):- contrar(X,Xs).

contrar($X,[X|_]).

 contrar($X,[_|Xs]):- contrar($X,Xs).

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

5. Функция soed. Объединяет два дизъюнкта с учетом контрарности

Реализация процедуры заключается в том, что сначала сравнивается каждый элемент первого списка с элементами второго списка, если элемент удовлетворяет поставленным условиям, то он записывается результат и вызывается рекурсивно soed для хвоста первого списка, второго списка и полученного результата. Таким образом, второй аргумент является списком-константой, а все операции выполняются над первым списком (общий случай).

Рассмотрим три возможных случая:

а) Если первый элемент первого списка не принадлежит и не имеет контрарных атомов во втором списке, то записать его в список-результат и вызывать soed рекурсивно, где первый аргумент - хвост, второй остаётся без изменения, а третий получаем путём добавления просматриваемого элемента.

б) Если первый элемент принадлежит второму списку, то сразу же вызывать soed с теми же параметрами, только в качестве первого аргумента необходимо передать его хвост.

в) Если во втором списке есть контрарный атом, то его нужно удалить из второго списка и вызвать рекурсивно soed с хвостом первого списка, результатом удаления контрарного атома во втором списке и результатом в качестве третьего параметра.

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

 soed([],X,X).

soed([X|Xs],Y,[X|Z]):- not(vhodit(X,Y)), not(contrar(X,Y)), soed(Xs,Y,Z).

soed([X|Xs],Y,Z):- vhodit(X,Y), soed(Xs,Y,Z).

soed([X|Xs],Y,Z):- contrar(X,Y), udalit($X,Y,D), soed(Xs,D,Z).

soed([$X|Xs],Y,[$X|Z]):- not(vhodit($X,Y)), not(contrar($X,Y)), soed(Xs,Y,Z).

soed([$X|Xs],Y,Z):- vhodit($X,Y), soed(Xs,Y,Z).

soed([$X|Xs],Y,Z):- contrar($X,Y), udalit(X,Y,D), soed(Xs,D,Z).

Итак, получили все возможные комбинации дизъюнктов и функцию объединения двух резольвент. Теперь необходимо найти такую комбинацию, которая дает в результате пустую резольвенту. Организуем проверку. Для того чтобы начать проверку, необходимо использовать soed последовательно для каждого возможного варианта из всех комбинаций, так как в среде SWI-Prolog результат от функции perestanovka получается не сразу, а поочередно, поэтому для реализации проверки логического следования, будет достаточно написать проверку одного из возможных вариантов списка списков.

Сначала нужно исходный список разбить на голову и хвост, передать их другой функции prov арности 2, как 2 аргумента, и объединять первый аргумент со вторым функцией soed. Далее нужно вызвать рекурсивно функцию prov, взяв в качестве второго аргумента ее хвост и повторять, пока там не окажется пустой список.

nachprov([X|Xs]):- prov(X,Xs).

prov([], _).

prov(X,[Y|Ys]):- soed(X,Y,Z), prov(Z,Ys).

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

Функция pusk формирует все возможные комбинации перестановок, и проверяет возможный вариант на наличие пустой резольвенты. Если такая найдена, то проверка останавливается и возвращается результат True, иначе False программа проверяет следующий

Реализация алгоритма на языке Haskell

Рассмотрим тот же алгоритм и реализуем его на Haskell.

Для начала определим операцию логического отрицания. Haskell функциональный язык, поэтому гораздо легче представить операцию логического отрицания, как работу со строками, то есть, если есть литер «А», то контрарный ему литер будет образован путём сцепления двух символов ~ и A, которые в результате образуют «~A». Для сцепления будет пользоваться стандартной операцией «++».

Также необходимо определить функцию, определяющую контрарный атом. Если литер с отрицанием, то отсекаем голову, иначе добавляем в начало символ ~, обозначающий логическое отрицание.

cont x

|(head x == '~') = tail x

|otherwise = "~" ++ x

1. Функция perestanovka. Реализация этой функции отличается от той реализации, которая была представлена на Prolog. Реализация данной функции основывается на реверсировании возможных хвостов и последующем сцеплении со всеми подсписками возможных списков. Чтобы ее организовать, необходимы три функции, каждая из которых будет отвечать за определённое действие.

perestanovka :: Eq(a)=> [a]->[[a]]

perestanovka [] = [[]]

perestanovka (x: xs) = scep x (perestanovka xs)

scep :: Eq(a)=> a->[[a]]->[[a]]

scep x [[]] = [[x]]

scep x [] = []

scep x (h: t) = (rev x h)++( scep x t)

rev :: a->[a]->[[a]]

rev x [] = []

rev x h = [(x :h),(reverse (x: h))]

Функция rev формирует две последовательности нового списка: прямую и обратную. Если преобразуемый список - пустой список, то результатом будет пустой список (базовый случай). Иначе формируется список, который состоит из двух списков: первый сформирован добавлением первого аргумента к списку, а второй, реверсированием первого списка.

Функция scep. Эта функция «перемножает» первый аргумент на список, в результате которого возвращается список списков. Для корректного выхода, необходимо два базовых случая:

а) условие перемножения пустого списка на некоторую переменную,

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

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

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

3.Функция contrar. Она также как и в Prolog определяет наличия в списке контрарного атома заданному.

srav x y = if (( "~" ++ x == y) || ( "~" ++ y == x)) then True else False

contrar :: String -> [String] -> Bool

contrar x [] = False

contrar x y = if (srav x (head y) == True) then True else contrar x (tail y)

Первая функция нужна для проверки, являются ли атомы контрарными. Принцип работы основан на отделении первого символа.

Функция contrar состоит из двух случаев. Первый является базовым, и определяет поведение, если второй аргумент равен пустому списку. Основной случай аналогичен Prolog, смотрим, являются ли голова контрарным литером по отношению к рассматриваемому, если нет, то рекурсивно вызываем функцию для хвоста.

4. Функция soed. Ее структура будет отличаться от структуры в Prolog только синтаксической реализацией, вызванной тем, что любая функция возвращает значение, которое можно дальше использовать в программе.

soed :: [String] -> [String] -> [String]

soed [] x = x

soed x y

|(x == []) = x

|(not (elem (head x) y)) && (not (contrar (head x) y))

= (head x) : soed (tail x) y

|contrar (head x) y = soed (tail x) (delete (cont (head x)) y)

|otherwise = soed (tail x) y

Условия те же что и в Prolog, только в Haskell рассматривается один случай, так как при работе со строками, определена функцию, возвращающая контрарный атом, независимо от знака литера.

Итак, теперь перейдем к проверке. Процедура prov не остановится при обнаружении пустой резольвенты, так как в функциях языка Haskell возвращается конечное значение, а не производится поиск условий, успешного завершения работы функции. Поэтому необходимо переработать функцию так, чтобы после каждого вызова soed она проверяла, равен ли результат []. Если это так, то необходимо прервать выполнение алгоритма. Для простоты проверки и удобства записи, пусть функция nachprov арности 1 вызовет pr с двумя аргументами, головой проверяемого списка и с его хвостом:

nachprov [] = True

nachprov (x:xs) pr x xs

pr x (y:ys)

|x == [] = True

|ys == [] = if (soed x y) == [] then True else False

|otherwise = pr (soed x y) ys

Рассмотрим структуру вспомогательной функции pr. Если в неё передаётся пустой параметр в качестве первого аргумента, значит (при корректном вводе данных) это результат функции soed. Следовательно, при рассматриваемой комбинации, пустая резольвента найдена и мы завершаем работу с положительным результатом. В другом случае объединяем голову с результатом выполнения, вполне возможно, что хвост станет пустым. Рассмотрим этот случай отдельно: если до того как хвост стал равным [] в результате функции оказался тоже пустой список, значит пустая резольвента найдена. В противном случае мы рекурсивно вызываем goprov, как и во всех остальных случаях.

Для удобства запуска реализуем операцию pusk, которая принимает входной список, формирует комбинации и проверяет каждый из вариантов.

pusk x = prov (perestanovka x)

Эта функция выдаст ответ True или False.

Примеры работы программ

1. Пример работы программы на языке Prolog:

? - pusk ([[a, s, $b, $c], [$a, b], [$s, c]]).

Yes

? - pusk ([[a, s, $b, $c], [$a, $b], [$s, c]]).

No

3. Пример работы программы на языке Haskell:

Main > pusk ([[«a», « s», «~b», «~c»], [«~a», «b»], [«~s», «c»]]).

True

Main > pusk ([[«a», « s», «~b», «~c»], [«~a», «~b»], [«~s», «c»]]).

False

Заключение

Итак, цель курсовой работы достигнута: проверка логического следования методом резолюции на Prolog и на Haskell реализована. Задачи исправно работают. Материал пройденный на лекциях закреплен.

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

1. Братко И., Программирование на языке Пролог для искусственного интеллекта [Текст - Москва, "МИР", 1990.

2. Роганова Н.А., Функциональное программирование [Текст] - ГИНФО, 2002.

Приложение А

Листинг программы на языке Prolog

$($X):- X.

vhodit(X, [X|_]).

vhodit(X,[_|Xs]):- vhodit(X, Xs).

udalit(X,[X|Xs],Xs).

udalit(X,[Y|Ys],[Y|Z]):- udalit(X,Ys,Z).

contrar(X,[$X|_]).

contrar(X,[_|Xs]):- contrar(X,Xs).

contrar($X,[X|_]).

contrar($X,[_|Xs]):- contrar($X,Xs).

perestanovka([], []).

perestanovka(Z,[X|K]):- udalit(X,Z,Z1), perestanovka(Z1,K).

soed([],X,X).

soed([X|Xs],Y,[X|Z]):- not(vhodit(X,Y)), not(contrar(X,Y)), soed(Xs,Y,Z).

soed([X|Xs],Y,Z):- vhodit(X,Y), soed(Xs,Y,Z).

soed([X|Xs],Y,Z):- contrar(X,Y), udalit($X,Y,D), soed(Xs,D,Z).

soed([$X|Xs],Y,[$X|Z]):- not(vhodit($X,Y)), not(contrar($X,Y)), soed(Xs,Y,Z).

soed([$X|Xs],Y,Z):- vhodit($X,Y), soed(Xs,Y,Z).

soed([$X|Xs],Y,Z):- contrar($X,Y), udalit(X,Y,D), soed(Xs,D,Z).

nachprov([X|Xs]):- prov(X,Xs).

prov([], _).

prov(X,[Y|Ys]):- soed(X,Y,Z), prov(Z,Ys).

pusk(X) :- perestanovka(X, Z), nachprov(Z).

Приложение Б

Листинг программы на языке Haskell

cont :: String -> String

cont x

|(head x == '~') = tail x

|otherwise = "~" ++ x

srav :: String -> String -> Bool

srav x y = if (( "~" ++ x == y) || ( "~" ++ y == x)) then True else False

contrar :: String -> [String] -> Bool

contrar x [] = False

contrar x y = if (srav x (head y) == True) then True else contrar x (tail y)

perestanovka :: Eq(a)=> [a]->[[a]]

perestanovka [] = [[]]

perestanovka (x:xs) = scep x (perestanovka xs)

scep :: Eq(a)=> a->[[a]]->[[a]]

scep x [[]] = [[x]]

scep x [] = []

scep x (h:t) = (rev x h)++(scep x t)

rev :: a->[a]->[[a]]

rev x [] = []

rev x h = [(x:h),(reverse (x:h))]

soed :: [String] -> [String] -> [String]

soed [] x = x

soed x y

|(x == []) = x

|(not (elem (head x) y)) && (not (contrar (head x) y))

= (head x) : soed (tail x) y

|contrar (head x) y = soed (tail x) (delete (cont (head x)) y)

|otherwise = soed (tail x) y

nachprov :: [[String]] -> [String]

nachprov [] = True

nachprov (x:xs) = pr x xs

pr x (y:ys)

|x == [] = True

|ys == [] = if (soed x y) == [] then True else False

|otherwise = pr (soed x y) ys

prov [] = False

prov x

|nachprov (head x) = True

|otherwise = prov (tail x)

pusk x = prov (perestanovka x)

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