Проверка логического следования методом резолюции
Курсовой проект - Компьютеры, программирование
Другие курсовые по предмету Компьютеры, программирование
естановку его хвоста - получаем некий список K, затем добавляем X в его начало.
2.Функция udalit. Удаляет элемент из списка.
udalit(X,[X|Xs],Xs).(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(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 [] = [[]](x: xs) = scep x (perestanovka xs):: Eq(a)=> a->[[a]]->[[a]]x [[]] = [[x]]x [] = []x (h: t) = (rev x h)++( scep x t):: a->[a]->[[a]]x [] = []x h = [(x :h),(reverse (x: h))]
Функция rev фо