ustify"> резолютивну висновок 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. Провести об'єднання диз'юнктів з урахуванням контрарності.
Необхідна така операція В«об'єднанняВ», яка враховуватиме контрарность литеров.
Якщо вводиться стартова послідовність (комбінація) диз'юнктів утворює порожню резольвенту, то перевірка логічного проходження...
