- •Введение
- •Занятие 1. Основные понятия математической логики. Исчисление высказываний
- •1.1. Введение
- •1.2. Исчисление высказываний
- •1.2.1. Основные логические функции исчисления высказываний
- •1.2.2. Дизъюнктивно-нормальная и конъюнктивно- нормальная формы
- •Контрольные вопросы и упражнения
- •Занятие 2. Перевод высказываний естественного языка на язык исчисления высказываний
- •Контрольные вопросы и упражнения
- •Занятие 3. Логический вывод в исчислении высказываний
- •3.1. Силлогизмы
- •3.2. Метод прямого преобразования
- •3.3. Метод семантических таблиц
- •3.4. Метод резолюций
- •Метод насыщения уровня
- •3.4.2. Стратегия вычеркивания
- •Контрольные вопросы и упражнения
- •Занятие 4. Исчисление предикатов
- •4.1. Основные понятия
- •4.2. Кванторные операции
- •4.3. Равносильности логики предикатов
- •4.4. Предваренная, сколемовская нормальная и сколемовская стандартная формы
- •Контрольные вопросы и упражнения
- •Занятие 5. Перевод высказываний естественного языка на язык логики предикатов
- •Контрольные вопросы и упражнения
- •Занятие 6. Логическое следствие в исчислении предикатов
- •6.1. Метод семантических таблиц
- •6.2. Процедура вывода Эрбрана
- •6.3. Принцип резолюции
- •6.3.1. Алгоритм унификации
- •6.3.2. Метод резолюций в исчислении предикатов
- •Контрольные вопросы и упражнения
- •Занятие 7. Теория алгоритмов
- •7.1. Вычислимые функции, частично-рекурсивные и общерекурсивные функции. Тезис Черча
- •7.2. Машинная математика. Машина Тьюринга.
- •7.3. Тезис Тьюринга (основная гипотеза теории алгоритмов)
- •7.4. Нормальные алгоритмы Маркова
- •Занятие 8. Обзор неклассических логик
- •8.1. Нечеткая логика
- •8.2. Модальные логики
- •8.3. Временные (темпоральные) логики
- •Заключение
- •Библиографический список
- •Оглавление
- •394026 Воронеж, Московский просп., 14
6.1. Метод семантических таблиц
Для доказательства правильности умозаключения в исчислении предикатов можно пользоваться методом семантических таблиц. Как и в исчислении высказываний с помощью семантической таблицы можно доказать общезначимость формулы.
Основой для построения семантических таблиц является атомарная семантическая таблица.
На основании атомарной семантической таблицы докажем общезначимость формулы
|
|
|
|
|
Формула является общезначимой, так как соответствующая ей семантическая таблица, построенная в предположении ложности формулы, является противоречивой.
Таблица 4
|
|
|
|
99
Продолжение табл. 4
|
|
|
|
|
|
|
|
|
|
|
Построим семантическую таблицу для формулы .
|
|
|
|
100
Данная семантическая таблица не является противоречивой, поскольку функция истинна при каком-то одном значении из области определения функции и та же функция ложна при каком-то другом значении . Для всех же значений условие противоречивости не выполняется.
Далее приведены семантические таблицы для двух общезначимых формул.
|
|
|
|
|
|
|
| |
101
| |
| |
| |
|
| |
6.2. Процедура вывода Эрбрана
Раннее было установлено, что множество дизъюнктов невыполнимо тогда и только тогда, когда оно принимает значение ложь при всех интерпретациях на любых областях. Однако в силу невозможности рассмотрения всех интерпретаций на любых областях хорошо бы найти такую специальную область интерпретации, установив на которой факт невыполнимости множества дизъюнктов, можно было бы сделать вывод о невыполнимости этого множества на любых других областях интерпретаций.
102
Такая специальная область интерпретации существует и называется универсумом Эрбрана. Универсум Эрбрана определяется так:
Шаг 1. Пусть - множество дизъюнктов, соответствующее предложению .
где - новая константа (слово “новая означает, что она не встречается в ). Эта новая константа выбирается произвольным образом.
Шаг .
И, наконец, полагаем .
Множество всех термов, построенных из констант и функциональных символов, встречающихся в , называется эрбрановским универсумом для , а – его уровнем . Множества называются эрбрановскими множествами
Проиллюстрируем получение универсума Эрбрана на следующих примерах.
Пример 1. Пусть
Тогда
;
;
;
…………………………………….
.
103
Пример 2.
Пусть
Так как не существует никаких констант в , полагаем . Не существует никаких функциональных символов в , следовательно,
Пример 3.
Пусть .
Тогда ;
;
;
………………………………………………………
.
Пример 4.
Пусть ;
;
;
.
………………………………………………………
Если под выражением понимать терм, множество термов, атом, множество атомов, литеру, множество литер, дизъюнкт или множество дизъюнктов, то под фундаментальным выражением будем понимать выражение, в котором все переменные заменены элементами универсума Эрбрана. Так, фундаментальным примером дизъюнкта будем называть дизъюнкт, полученный заменой всех переменных в этом дизъюнкте элементами универсума Эрбрана таким образом, что все вхождения одной и той же переменной в дизъюнкт заменяются одним и тем же элементом универсума.
104
Множество фундаментальных атомов вида , где – все - местные предикатные символы, встречающиеся во множестве дизъюнктов и – элементы универсума Эрбрана, называется атомарным множеством или эрбрановской базой для . Обозначим эрбрановскую базу через .
Пример 5.
Пусть .
Тогда
Фундаментальные примеры: и т.п.
Определим теперь интерпретацию на универсуме Эрбрана и назовем ее - интерпретацией. Говорят, что интерпретация является - интерпретацией для множества дизъюнктов , если выполнены следующие соответствия:
- каждому предикатному символу соответствует некоторое - местное отношение в ;
- каждому функциональному символу соответствует некоторая - местная функция в (т.е. функция, отображающая в );
- каждой предметной константе из соответствует некоторая константа из (т.е. все константы отображаются на самих себя).
Пусть является эрбрановской базой для . Тогда - интерпретация может быть представлена множеством , в котором есть или для При этом, если есть то имеет значение “истина”, в противном случае “ложь”.
105
Пример 6. Пусть .
Тогда .
Примеры - интерпретаций:
; ; При оба дизъюнкта выполнимы, при первый дизъюнкт выполним, второй нет, при оба дизъюнкта невыполнимы, т.е. принимают значение “ложь”.
В случае если интерпретация задана не на универсуме Эрбрана, а на произвольной области , то можно установить следующее соответствие между этими интерпретациями. Пусть дана интерпретация на некоторой области . Говорят, что - интерпретация соответствует интерпретации , если имеет место следующее: пусть – элементы и пусть каждый отображается на некоторый элемент области , тогда, если любой принимает значение “истина” (“ложь”) при интерпретации , то также принимает значение “истина” (“ложь”) при . Имеет место следующая теорема.
Теорема Множество дизъюнктов невыполнимо тогда и только тогда, когда ложно при всех - интерпретациях.
Доказательство «тогда» очевидно, а «только тогда» легко доказывается от противного введением соответствия между - интерпретацией и некоторой произвольной
106
интерпретацией. В дальнейшем будем рассматривать только
- интерпретации, и называть их просто интерпретациями .
Таким образом, для установления невыполнимости множества дизъюнктов необходимо и достаточно рассмотреть только - интерпретации.
Процедура вывода Эрбрана основывается на его теореме.
Теорема Эрбрана. Множество дизъюнктов невыполнимо тогда и только тогда, когда существует конечное невыполнимое множество фундаментальных примеров дизъюнктов .
Таким образом, для установления невыполнимости множества дизъюнктов необходимо образовать множества фундаментальных примеров дизъюнктов и последовательно проверять их на ложность. Теорема Эрбрана гарантирует, что, если множество дизъюнктов невыполнимо, то данная процедура обнаружит такое , что является ложным.
Процедура вывода Эрбрана состоит из двух этапов: сначала находится множество всех фундаментальных примеров дизъюнктов и затем, используя мультипликативный метод, из КНФ получают ДНФ.
Пример.
Пусть .
Находим
и фундаментальные примеры дизъюнктов:
.
Затем с помощью мультипликативного метода убеждаемся в невыполнимости .
107
= .
Недостаток процедуры вывода Эрбрана состоит в экспоненциальном росте множества фундаментальных примеров при увеличении . C помощью процедуры вывода Эрбрана удается доказать только простые теоремы.
Иной поход предложил Дж. Робинсон, который ввел принцип резолюции, являющийся теоретической базой для построения большинства методов автоматического доказательства теорем.