- •Математическая логика и теория алгоритмов
- •Воронеж 2011
- •1. Логика высказываний
- •1.1. Алгебра высказываний
- •Операции над высказываниями
- •1.1.2. Правила записи сложных формул
- •1.1.3. Таблицы истинности
- •1.1.4. Равносильность формул
- •1.1.5. Дизъюнктивные и конъюнктивные нормальные формы
- •1.1.6. Логическое следствие
- •1.2. Исчисление высказываний
- •1.2.1. Алгоритмы проверки общезначимости и противоречивости в исчислении высказываний
- •1.2.2. Метод резолюций в исчислении высказываний
- •1.2.3. Метод резолюций для хорновских дизъюнктов
- •Задачи и упражнения
- •2. Логика и исчисление предикатов
- •2.1. Логика предикатов
- •2.2. Алгебра предикатов
- •2.2.1. Логические операции
- •2.2.2. Правила записи сложных формул
- •2.2.3. Законы алгебры предикатов
- •2.2.4. Предваренная нормальная форма
- •2.2.4.1. Алгоритм приведения формулы к виду пнф
- •2.2.5. Сколемовская стандартная форма
- •2.2.5.1. Алгоритм Сколема
- •2.3. Исчисление предикатов
- •2.3.1. Интерпретация формул
- •2.3.2. Правила вывода
- •2.3.3. Метод дедуктивного вывода
- •2.3.4. Метод резолюций в исчислении предикатов
- •2.4. Проблемы в исчислении предикатов
- •2.5. Логическое программирование
- •Задачи и упражнения
- •3. Элементы теории алгоритмов
- •3.1. Рекурсивные функции
- •3.1.1. Базовые функции
- •3.1.2. Элементарные операции
- •Выразим с помощью схемы примитивной рекурсии:
- •3.2. Машина Тьюринга
- •3.2.1. Описание машины Тьюринга
- •3.2.2. Примеры машин Тьюринга
- •3.3. Конечные автоматы
- •4. Неклассические логики
- •4.1. Пропозиционные логики
- •4.2. Алгоритмические логики
- •Задачи и упражнения
- •Заключение
- •Библиографический список
- •Оглавление
- •394026 Воронеж, Московский просп., 14
1.2.1. Алгоритмы проверки общезначимости и противоречивости в исчислении высказываний
1. Алгоритм Квайна. Напомним, что формула F от пропозициональных переменных А1, А2, …, Аn является общезначимой (тождественно истинной) или (что то же самой) доказуемой, если булева функция , соответствующая формуле F, тождественно равна 1. Для проверки значений функции f используется так называемое семантическое дерево, т.е. бинарное дерево, которое удовлетворяется следующим условиям:
каждое ребро соответствует переменной (с отрицанием или без);
ребра, выходящие из одной вершины, соответствуют контрарным переменным: , ;
ребра соответствуют одной и той же переменной тогда и только тогда, когда они находятся на одинаковом расстоянии от корня (рис. 1.1).
Семантическое дерево имеет висячих вершин и для проверки общезначимости необходимо пройти маршрутов от корня до этих вершин.
Алгоритм Квайна позволяет проходить не все семантическое дерево, а только его часть. Он состоит в том, что пропозициональным переменным , упорядоченным в набор (А1,А2, …, Аn), последовательно придают значения 0 и 1 и анализируют таблицы истинности формул, содержащих меньшее число переменных.
Пример. Проверить общезначимость формулы
.
Упорядочим пропозициональные переменные (А, В, С). Придадим первой переменной А значение 1, т.е. А=1. Тогда формула F преобразуется следующим образом:
.
В полученной формуле переменной В придадим значение 1, т.е. В=1. Тогда преобразованная формула имеет вид , т.е. будет общезначимой. В случае В=0 имеем , что также общезначимо. Рассмотрим теперь случай А=0. Имеем
.
Таким образом, все возможные случаи приводят к тождественно истинным (общезначимым) формулам. Следовательно, формула F также истинна. На рис. 1.2а изображено семантическое дерево, соответствующее формуле F, а на рис. 1.2б показана часть семантического дерева, которая фактически использовалась для проверки общезначимости.
2. Алгоритм редукции решает ту же задачу проверки общезначимости формулы, но используется в том случае, когда в формуле содержится достаточно много импликаций. Идея алгоритма состоит в попытке нахождения значений пропозициональных переменных формулы F, при которых значение функции f равно 0, на основе того, что импликация является ложной в том и только в том случае, когда посылка истинна, а заключение ложно.
Пример. Проверить тождественную истинность формулы
Предположим, что формула ложна при некотором наборе значений переменных А, В, С. Тогда истинностная функция f по этим значениям переменных дает следующие значения формул: , . Тогда из второго равенства получает А=1, , откуда имеем B=1, C=0. Однако при этих значениях справедливо . Получили противоречие. Таким образом, формула F тождественно истинна.