DataLife Engine > Версия для печати > Перевірка логічного проходження методом резолюції

Введення

У цій роботі буде розглянуто алгоритм перевірки логічного проходження методом резолюції. Його реалізація буде представлена вЂ‹вЂ‹па логічному мовою Prolog і на функціональному мовою Haskell. p align="justify"> Метод резолюції - метод доведення теорем в теоріях першого порядку, що використовує правило висновку, зване резолюцією.

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

Мета даної курсової роботи полягає в тому, що необхідно написати програми на двох мовах, реалізують алгоритм перевірки логічного проходження методом резолюції, і закріпити на лекціях матеріал.

Для вирішення поставленої мети необхідно вирішити такі завдання:

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

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

) реалізувати його на мові Prolog;

) реалізувати алгоритм на мові Haskell.

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

Постановка завдання

Отже, розглянемо алгоритм перевірки логічного проходження методом резолюції. Для початку необхідно розглянути принцип резолюції. Припустимо, є безліч диз'юнктів - D, які представляють певну формулу F. Формула F суперечлива тоді і тільки тоді, коли суперечливо безліч диз'юнктів D. Якщо в безлічі D мається порожній диз'юнкт, то воно не здійснимо. Якщо в цій безлічі немає порожнього диз'юнктів, то перевіряється можливість отримання порожнього диз'юнктів з нього. Метод резолюції можна застосувати до будь-якого безлічі диз'юнктів, щоб перевірити їх суперечливість. p align="justify"> Літери L і ~ L називаються контрарними, а безліч {L, ~ L} - контрарной парою. Якщо в диз'юнктів D 1 існує літера L 1 , контрарності літері L 2 в диз'юнктів D 2 , то необхідно видалити літери L 1 і L 2 з диз'юнктів D 1 і D 2 відповідно і побудувати диз'юнкцію залишилися диз'юнктів. Одержаний диз'юнкт називається резольвенти.

резолютивну висновок L з безлічі диз'юнктів D є така кінцева послідовність L 1 , L 2 , ..., 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]], де квадратні дужки визначають диз'юнкт, коми у них поділяють літери диз'юнктів. Дана структура найбільш підходяща для цього завдання, тому що ефективна в реалізації функцій завдання. Наприклад, перестановка не вимагає повної реконструкції структури, необхідно тільки застосування операцій видалення, вставки, об'єднання диз'юнктів з такою структурою реалізується просто, при чому з урахуванням контрарності. p align="justify"> Звичайно, можна використовувати й іншу структуру таку, як дерево, але це буде складно і громіздко, так як кількість операцій залежить від кількості диз'юнктів і від кількості литеров в них, а подання дерев з великою кількістю гілок складно і витрата пам'яті буде набагато більше, ніж при використанні структури В«список списківВ».

Формулювання алгоритму

Отже, розглянемо етапи рішення задачі.

1. Шукати всі можливі комбінації диз'юнктів.

Необхідно враховувати, що при перевірці логічного проходження методом резолюції на результат впливає послідовність диз'юнктів. Мета даної роботи полягає в пошуку тієї послідовності диз'юнктів, яка в результаті утворює порожню резольвенту. p align="justify"> 2. Провести об'єднання диз'юнктів з урахуванням контрарності.

Необхідна така операція В«об'єднанняВ», яка враховуватиме контрарность литеров.

Якщо вводиться стартова послідовність (комбінація) диз'юнктів утворює порожню резольвенту, то перевірка логічного проходження... закінчена з позитивним результатом.

Недолік алгоритму: якщо порожня резольвента знайдена, а диз'юнктів були задіяні не всі, то операція об'єднання не припинить виконання пошуку, а продовжить свою роботу. Тому необхідно використовувати змінну, яка буде повідомляти при знайденої порожній резольвент про кінець роботи алгоритму. p align="justify"> Отже, розглянувши алгоритм вирішення задачі, перейдемо до його реалізації на мові Prolog і мовою Haskell.

Реалізація алгоритму мовою Prolog

Для початку необхідно визначити відношення між атомами (контрарность). За законом математичної логіки, можна ввести наступне твердження: $ ($ X): - X, де символ $ буде схематичне записом заперечення, оскільки в деяких версіях SWI-Prolog, символ ~ зарезервований. p align="justify"> Отже, розглянемо функції, за допомогою яких будемо реалізувати алгоритм:

1. Функція perestanovka. Породжує всі можливі перестановки

елементів списку.

perestanovka ([], []).

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

Якщо перший список порожній, то результат порожній (базовий випадок). Інакше видаляємо голову X з першого списку, робимо перестановку його хвоста - отримуємо якийсь список K, потім додаємо X в його початок. p align="justify"> 2. Функція udalit. Видаляє елемент із списку.

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

Якщо елемент збігається з головою другого списку, то результатом буде хвіст списку (базовий випадок). Інакше результатом буде список голова, якого збігається з головою вихідного списку, а хвіст виходить видаленням заданого елемента з хвоста заданого списку. p align="justify"> 3. Функція vhodit. Перевіряє належність елемента до списку.

vhodit (X, [X | _]).

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

Елемент належить списку, якщо він порівнянний з головою списку (базовий випадок). Інакше елемент належить хвосту другого списку. p align="justify"> 4 Функція contrar. Перевіряє контрарность литеров. Prolog-машина сприймає X і $ X як два різних вирази, так як $ X тобто не літер, а результат функції $. Тому розглядаються два випадки, які розрізняються контрарності перших елементів. br/>

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

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

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

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

Елемент має контрарності пару, якщо голова списку є контрарності елементом для заданого елемента (базовий випадок...). Інакше контрарний елемент належить хвосту другого списку. p align="justify"> 5. Функція soed. Об'єднує два диз'юнктів з урахуванням контрарності

Реалізація процедури полягає в тому, що спочатку порівнюється кожен елемент першого списку з елементами другого списку, якщо елемент задовольняє поставленим умовам, то він записується результат і викликається рекурсивно soed для хвоста першого списку, другого списку і отриманого результату . Таким чином, другий аргумент є списком-константою, а всі операції виконуються над першим списком (загальний випадок). p align="justify"> Розглянемо три можливі випадки:

а) Якщо перший елемент першого списку не належить і не має контрарних атомів в другому списку, то записати його в список-результат і викликати 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, взявши в якості другого аргументу її хвіст і повторювати, поки там не виявиться порожньою список. br/>

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

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

Базовим випадком другої функції є умова, коли перший аргумент є порожня функція. Воно виходить в тому випадку, якщо буде знайдена порожня резольвента, тобто пошук закінчений з успіхом. p align="justify"> Функція pusk формує всі можливі комбінації перестановок, і перевіряє можливий варіант на наявність порожній резольвенти. Якщо така знайдена, то перевірка зупиняється і повертається результат True, інакше False програма перевіряє наступний

Реалізація алгоритму мовою Haskell

Розглянемо той же алгоритм і реалізуємо його на Haskell.

Для початку визначимо операцію логічного заперечення. Haskell функціональний мова, тому набагато легше уявити операцію логічного заперечення, як роботу з рядками, тобто, якщо є літер В«АВ», то контрарний йому літер буде утворений шляхом зчеплення двох символів ~ і A, які в результаті утворюють В«~ AВ». Для зчеплення буде користуватися стандартною операцією В«+ +В». p align="justify"> Також необхідно визначити функцію, що визначає контрарний атом. Якщо літер з запереченням, то відсікаємо голову, інакше додаємо в початок символ ~, що позначає логічне заперечення. p align="justify"> cont x

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

| otherwise = "~" + + x

1. Функція perestanovka. Реалізація цієї функції відрізняється від тієї реалізації, яка була представлена вЂ‹вЂ‹на Prolog. Реалізація даної функції грунтується на реверсуванні можливих хвостів і наступному зчепленні з усіма підсписків можливих списків. Щоб її організувати, необхідні три функції, кожна з яких відповідатиме за певну дію. p align="justify"> perestanovka :: Eq (a) => [a] -> [[a]]

perestanovka [] = [[]] (x: xs) = scep x (perestanovka xs) :: Eq (a) => a-> [[a]] -> [ [a]] x [[]] = [[x]] x [] = [] x (h: t) = (rev xh) + + (scep xt) :: a-> [a] -> [[a]] x [] = [] xh = [(x: h), (reverse (x: h))]

Функція rev формує дві послідовності нового списку: прямий і зворотний. Якщо преутворений список - порожній список, то результатом буде порожній список (базовий випадок). Інакше формується список, який складається з двох списків: перший сформований додаванням першого аргументу до списку, а другий, реверсированием першого списку. p align="justify"> Функція scep. Ця функція В«перемножуєВ» перший аргумент на список, в результаті якого повертається список списків. Для коректного виходу, необхідно два базових випадку:

а) умова перемноження порожнього списку на деяку змінну,

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

В окремому випадку виробляємо зчеплення першого аргументу з головою другого аргументу (сформували перший результуючий елемент) з рекурсивно викликаної функцією scep для того ж першого аргументу і хвоста другого аргументу.

Наприкінці формуються всі комбінацій викликом функції perestanovka, яка рекурсивно зчіплює свою голову з рекурсивно викликаної perestanovka, яка має в якості аргументу хвіст. Комбінація порожнього списку, є порожній список списків (базовий випадок). p align="justify">. Функція contrar. Вона також як і в Prolog визначає наявності у списку контрарного атома заданому. br/>

srav xy = if (("~" + + x == y) | | ("~" + + y == x)) then True else False :: String - > [String] -> Boolx [] = False

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

Перша функція потрібна для перевірки, чи є атоми контрарними. Принцип роботи заснований на відділенні першого символу. p align="justify"> Функція contrar складається з двох випадків. Перший є базовим, і визначає поведінку, якщо другий аргумент дорівнює пустому списку. Основний випадок аналогічний Prolog, дивимося, чи є голова контрарності Літері стосовно розглянутого, якщо ні, то рекурсивно викликаємо функцію для хвоста. p align="justify"> 4. Функція soed. Її структура буде відрізнятися від структури в Prolog тільки синтаксичної реалізацією, викликаної тим, що будь-яка функція повертає значення, яке можна далі використовувати в програмі. br/>

soed :: [String] -> [String] -> [String] [] x = xx 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 xy) == [] then True else False

| otherwise = pr (soed xy) ys

Розглянемо структуру допоміжної функції pr. Якщо в неї передається порожній параметр в якості першого аргументу, значить (при коректному введенні даних) це результат функції soed. Отже, при розглянутої комбінації, порожня резольвента знайдена і ми завершуємо роботу з позитивним результатом. В іншому випадку об'єднуємо голову з результатом виконання, цілком можливо, що хвіст стане порожнім. Розглянемо цей випадок окремо: якщо до того як хвіст став рівним [] в результаті функції виявився теж порожній список, значить порожня резольвента знайдена. В іншому випадку ми рекурсивно викликаємо goprov, як і у всіх інших випадках. p align="justify"> Для зручності запуску реалізуємо операцію pusk, яка приймає вхідний список, формує комбінації і перевіряє кожен з варіантів.

pusk x = prov (perestanovka x)

Ця функція видасть відповідь True або False.

Приклади роботи програм

1. Приклад роботи програми мовою Prolog:

? - Pusk ([[a, s, $ b, $ c], [$ a, b], [$ s, c]]). p align="justify">? - Pusk ([[a, s, $ b, $ c], [$ a, $ b], [$ s, c]]). p align="justify"> 3. Приклад роботи програми мовою Haskell:

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

Висновок

Отже, мета курсової роботи досягнута: перевірка логічного проходження методом резолюції на Prolog і на Haskell реалізована. Завдання справно працюють. Матеріал поданий на лекціях закріплений. br/>

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

1. Братко І., Програмування на мові Пролог для штучного інтелекту [Текст - Москва, "СВІТ", 1990. p align="justify"> 2. Роганова Н.А., Функціональне програмування [Текст] - ГІНФО, 2002. br/>

Додаток А

Лістинг програми на мові Prolog

Додаток Б

Лістинг програми на мові Haskell

cont :: String -> Stringx

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

| otherwise = "~" + + x :: String -> String -> Boolx y = if (("~" + + x == y) | | ( "~" + + y == x)) then True else False :: String -> [String] -> Boolx [] = Falsex y = if (srav x (head y) == True) then True else contrar x (tail y) :: Eq (a) => [a] -> [[a]] [] = [[]] (x: xs) = scep x (perestanovka xs) :: Eq ( a) => a-> [[a]] -> [[a]] x [[]] = [[x]] x [] = [] x (h: t) = (rev xh) + + (scep xt) :: a-> [a] -> [[a]] x [] = [] xh = [(x: h), (reverse (x: h))] :: [ String] -> [String] -> [String] [] x = xx 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 :: [[String]] -> [String] [] = True (x: xs) = pr x xsx (y: ys)

| x == [] = True

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

| otherwise = pr (soed xy) ys [] = Falsex

| nachprov (head x) = True

| otherwise = prov (tail x) x = prov (perestanovka x)