Введення
У цій роботі буде розглянуто алгоритм перевірки логічного проходження методом резолюції. Його реалізація буде представлена ​​па логічному мовою 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 відповідно і побудувати диз'юнкцію залишилися диз'юнктів. Одержаний диз'юнкт називається резольвенти.
