- •Математическая логика и теория алгоритмов
- •11. Понятие об алгоритмах. Схемы алгоритмов
- •11.1. Понятие об алгоритме и теории алгоритмов
- •11.2. Схемы алгоритмов
- •11.3. Рекурсивные функции
- •11.4. Машина Тьюринга
- •11.5. Машина Поста
- •11.6. Нормальные алгорифмы а.А. Маркова
- •11.7. Универсальная абстрактная машина
- •11.8. Разрешимость в теории алгоритмов. Проблема самоприменимости
- •11.9. Сложность алгоритма
- •11.10. Представление схемы алгоритма эквивалентным автоматом
- •11.11. Представление схемы алгоритма микропрограммой с двумя типами микрокоманд
- •12. Элементы формальной логики
- •12.1. Предмет формальной логики
- •12.2. Понятие и его виды
- •12.3. Отношения между понятиями
- •12.4. Операции над понятиями
- •12.5. Суждение и его характеристика
- •Модальные и категорические суждения.
- •Простые категорические суждения.
- •Виды простых категорических суждений.
- •Распределение терминов в простом категорическом суждении.
- •Логический квадрат.
- •13. Умозаключение
- •13.1. Виды умозаключений
- •13.2. Непосредственное умозаключение
- •Умозаключения путем противопоставления предикату.
- •13.3. Опосредованное дедуктивное умозаключение. Фигуры силлогизма
- •Фигуры пкс.
- •Модусы пкс.
- •13.4. Дополнительные виды силлогизмов
- •13.5. Индуктивные умозаключения. Математическая индукция
- •14. Логика высказываний
- •14.1. Семантика логики высказываний
- •I закон – тождества.
- •14.3. Формализация высказываний
- •14.4. Интерпретации, разрешимость, выполнимость, общезначимость
- •14. 5. Логическая равносильность. Законы логики
- •14.6. Формы представления формул логики высказываний
- •14.7. Проблема дедукции в логике высказываний
- •15. Проверка правильности логических выводов. Метод резолюций
- •15.1. Закон контрапозиции
- •15.2. Логическое следование. Проверка правильности логических выводов
- •15.3. Силлогизмы в логике высказываний
- •Разделительно-категоричные силлогизмы.
- •16. Синтаксис и семантика языка логики предикатов
- •16.1. Понятие предиката
- •16.2. Кванторы и связанные переменные
- •16.3. Синтаксис языка логики предикатов. Формулы логики предикатов и формализация суждений
- •16.4. Семантика формул логики предикатов
- •Общезначимость, выполнимость, невыполнимость.
- •17. Тождественные преобразования формул логики предикатов
- •17.1. Операции над предикатами
- •17.2. Основные равносильности логики предикатов
- •Отрицание предложений с кванторами.
- •17.3. Тождественные преобразования формул
- •17.4. Универсум Эрбрана
- •18. Использование метода резолюций в логике предикатов
- •18.1. Подстановка и унификация
- •18.2. Резольвенция и факторизация
- •18.3. Метод резолюций в логике предикатов
- •18.4. Принцип логического программирования
- •19. Логические исчисления
- •19.1. Понятие о формальных теориях
- •19.2. Исчисление высказываний
- •19.3. Исчисление предикатов
- •19.4. Система натурного вывода
- •19.5. Понятие о математической лингвистике
- •19.6. Формальный язык
- •19.7. Формальные грамматики и их свойства
- •19.8. Теоремы Гёделя
- •20. Неклассические логики
- •20.1. Современные модальные логики
- •20.2. Понятие о теории неопределенности
- •20.3. Элементы теории нечетких множеств и нечеткая логика
- •20.4. Нечеткие алгоритмы
- •Литература
- •Приложение 1 Варианты контрольных заданий по дисциплине «Дискретная математика»
- •Приложение 2 Варианты контрольных заданий по дисциплине «Математическая логика»
18.3. Метод резолюций в логике предикатов
Задача
установления невыполнимости множества
предложений в
Невыполнимая в частном случае формула не может быть выполнима в других случаях, так как формула замкнута, а замкнутая формула либо ложна, либо истинна. На этом и основано использование метода резолюции в логике предикатов.
Например, для умозаключения по модусу «Barbara» при использовании формализации [8]:
Получаем для умозаключения ААА по первой фигуре силлогизма конъюнкцию посылок и отрицания заключения: что соответствует
множеству дизъюнктов и дереву опровержения (рис. 120).
Рис. 120. Дерево опровержения для модуса «Barbara»
На рис. 120 «а» – это константа, получившаяся после введения функции Сколема при отрицании заключения модуса «Barbara».
Для модуса «Darapti» (третья фигура силлогизма) дизъюнкты и дерево опровержения имеют вид (рис. 121):
Рис. 121. Дерево опровержения для модуса «Darapti»
Опровержение не достигается, хотя модус правильный. Аналогично не достигается опровержение и для модусов «Felapton» и «Fesapo». Оказывается, это недостаток формализации, а не метода резолюций. В то же время формализация В.А. Смирнова [1]:
лишена этого недостатка. Так, для модуса «Felapton» (рис. 122):
Рис. 122. Дерево опровержения для модуса «Felapton»
и модели В.А. Смирнова
Непосредственной проверкой можно убедиться в том, что при этой формализации метод резолюции «работает» для всех 19-ти правильных основных и 5-ти дополнительных модусов [1] и не «работает» для остальных 232-х неправильных.
На методе резолюций основан язык логического программирования ПРОЛОГ.
18.4. Принцип логического программирования
В ряде логических задач [29] выясняют, следует ли логически некоторая формула F из множества Ф0.
В других задачах устанавливают значение элемента x (если оно существует!), при котором данная формула F, содержащая в качестве одного из аргументов x, следует из Ф0, т.е. сначала устанавливают, следует ли формула xF(x) из Ф0, а затем, при положительном ответе на этот вопрос, определяется соответствующее значение x.
Рассмотрим пример [29].
Пусть погрузочный работ (пр) располагается на автоматической тележке (ат). Тележка находится на складе (скл). Требуется ответить на вопрос, где находится погрузочный робот.
Формализуем задачу, введя предикат:
«Быть в определённом месте»: Б(z,x) – «z находится в x», тогда:
.
Первая формула выражает тот факт, что в каком бы месте не находилась тележка, в этом же месте находится погрузочный робот. Вторая формула – что тележка находится на складе.
Необходимо доказать теорему:
, т.е., что погрузочный робот где-то находится, и определить это соответствующее значение x.
Решение: получаем отрицание предположения: .
Получим множество дизъюнктов и применим метод резолюций:
,.
Рис. 123. Дерево опровержения для задачи о роботе
Таким образом, предположение следует из гипотез (рис. 123).
После построения дерева опровержения для извлечения ответа на поставленный вопрос строят модифицированное дерево доказательства:
1. К каждому предложению, вытекающему из отрицания предложения добавляются (в смысле дизъюнкции) его отрицания.
2. Выполняются те же самые резолюции, что и при построении дерева опровержения.
В корне модифицированного дерева доказательства получается частный случай предположения, который и используется в качестве ответа.
Рис. 124. Модифицированное дерево доказательства
для задачи о роботе
Таким образом, погрузочный робот находится на складе.
В процессе извлечения ответа возникают тавтологии (типа: ).
Но, т.к. тавтологию можно отбросить, не изменяя выполнимости или невыполнимости любого множества (конъюнкция с единицей), содержащего кроме тавтологии другие формулы, указанные предположения следуют из аксиом.
Таким образом, модифицированное дерево опровержения является графом доказательства того, что формула, расположенная в его корне, логически следует из аксиом.
Описанный процесс извлечения ответа можно применять при автоматическом построении простых программ для ЭВМ.
Пусть заданы отношения R(x,y) между x и y некоторым множеством аксиом, а также элементарные функции, определяемые другим множеством аксиом. Требуется написать программу, которая по заданным входным значениям выдает на выходе значение y, удовлетворяющая значению R(x,y). При её написании можно использовать заданные элементарные функции.
Требуемую программу можно построить с помощью процесса извлечения ответа, после того как будет доказано, что предположение логически следует из указанных аксиом. В корне модифицированного дерева доказательств будет ответное утверждение в виде композиции элементарных функций. Эта композиция и будет программой.