- •Математическая логика и теория алгоритмов
- •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 Варианты контрольных заданий по дисциплине «Математическая логика»
17.3. Тождественные преобразования формул
Формулы логики предикатов часто представляют в стандартной форме, например, в клаузальной. Формула в клаузальной форме (в виде конъюнкции – КНФ-дизъюнктов) явно использует лишь операции дизъюнкции, конъюнкции и инверсии, а каждый дизъюнкт – лишь операцию дизъюнкции и инверсии, причем инверсия применяется не более чем к одной предикатной букве (литере, литералу). Поэтому для представления произвольной формулы в форме дизъюнкта необходимо исключить все остальные логические операторы (включая кванторы) и уменьшить область действия знака отрицания до одной предикатной буквы [29].
Исключение знаков импликации.
Знаки импликации исключают, используя равносильность .
Например:
.
Уменьшение области действия знаков инверсии.
Это делается с помощью законов Де Моргана и правил инверсии выражений с кванторами.
Например:
Стандартизация переменных.
В области действия квантора связанную с ними переменную можно заменить произвольной переменной, не совпадающей с какой-либо другой переменной, входящей в область действия этих кванторов.
Например:
.
Однако, формулы ине равносильны.
Переименование связанных переменных формулы, при котором каждый квантор имеет собственную переменную, отличную от других, называется стандартизацией переменных.
Исключение кванторов существования.
В формуле , которую можно интерпретировать, например, как «для всехx существует такой y, что для x не больше y», квантор y находится внутри области действия квантора x. Поэтому y, который «существует», может зависеть от x. Эту зависимость в явной форме можно определить функцией g(x), отображающей каждое значение x в y. Такая функция называется функцией Сколема. Используя её, можно исключить квантор существования. Для обозначения функции Сколема не должны использоваться функциональные буквы, которые уже имеются в формуле. Если квантор существования находится в области действия двух и более кванторов общности, то функция Сколема будет зависеть соответственно от двух аргументов и более.
Если исключаемый квантор существования не принадлежит ни к одному квантору общности, то функция Сколема не содержит аргумента, т.е. является константой. Так, формула при исключении квантора существования преобразуется в формулу F(a), где а – константа, при которой известно, что формула F(a) «существует».
Операция исключения квантора существования называется ещё сколемизацией.
Исключение кванторов общности.
После исключения кванторов общности и стандартизации переменных формула содержит только кванторы общности, каждый из которых имеет свою переменную. Поэтому кванторы общности можно перенести в начало формулы (получаем предварённую формулу) и считать областью действия каждого квантора часть формулы, расположенную за ними. Например:
.
В связи с тем, что в импликации множество состоит из замкнутых формул, т.е. из формул, не содержащих свободных переменных, и формулаF замкнута, все переменные в формуле из будут относиться к кванторам общности. А так как порядок расположения кванторов общности не имеет значения, то эти кванторы можно явно не исключать, условившись, что все переменные в формуле относятся к кванторам общности.
Таким образом, кванторы исключают, получив предваренную форму из одних кванторов общности.
Представление формулы в КНФ.
Получение множества Ф1 (объединение формул ) эквивалентно КНФ соответствующей формулы. Так как какая-либо интерпретация удовлетворяет формуле видав том и только в том случае, если она удовлетворяет формулам и К1, К2, …, Кn одновременно, то исходную формулу Ф1 можно заменить множеством конъюнктивных членов (дизъюнктов).
Пример. .
Исключим знаки импликации:
.
Уменьшим области действия знаков отрицания до одного предиката:
.
Произведем стандартизацию переменных:
Проведем сколемизацию:
Здесь g(z) – функция Сколема, зависящая только от x, она находится в области действия квантора.
Получим предваренную форму формулы:
.
Исключим кванторы общности:
.
Используя закон дистрибутивности, получим КНФ:
.