закінчена з позитивним результатом.
Недолік алгоритму: якщо порожня резольвента знайдена, а диз'юнктів були задіяні не всі, то операція об'єднання не припинить виконання пошуку, а продовжить свою роботу. Тому необхідно використовувати змінну, яка буде повідомляти при знайденої порожній резольвент про кінець роботи алгоритму. 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).
Елемент має контрарності пару, якщо голова списку є контрарності елементом для заданого елемента (базовий випадок...
