Процедура вывода Эрбрана

Метод семантических таблиц

Для доказательства правильности умозаключения в исчислении предикатов можно пользоваться методом семантических таблиц. Как и в исчислении высказываний с помощью семантической таблицы можно доказать общезначимость формулы.

Основой для построения семантических таблиц является атомарная семантическая таблица.

На основании атомарной семантической таблицы докажем общезначимость формулы

|

|

|

|

|

Формула является общезначимой, так как соответствующая ей семантическая таблица, построенная в предположении ложности формулы, является противоречивой.

Таблица 4

Продолжение табл. 4

Построим семантическую таблицу для формулы .

|

|

|

|

Данная семантическая таблица не является противоречивой, поскольку функция истинна при каком-то одном значении из области определения функции и та же функция ложна при каком-то другом значении . Для всех же значений условие противоречивости не выполняется.

Далее приведены семантические таблицы для двух общезначимых формул.

|

|

|

|

|

|

|

| |

| |

| |

| |

| ½

| |

½

½ ½ ½

Å Å

Å Å

Раннее было установлено, что множество дизъюнктов невыполнимо тогда и только тогда, когда оно принимает значение ложь при всех интерпретациях на любых областях. Однако в силу невозможности рассмотрения всех интерпретаций на любых областях хорошо бы найти такую специальную область интерпретации, установив на которой факт невыполнимости множества дизъюнктов, можно было бы сделать вывод о невыполнимости этого множества на любых других областях интерпретаций.

Такая специальная область интерпретации существует и называется универсумом Эрбрана. Универсум Эрбрана определяется так:

Шаг 1. Пусть - множество дизъюнктов, соответствующее предложению .

где - новая константа (слово “новая означает, что она не встречается в ). Эта новая константа выбирается произвольным образом.

Шаг .

И, наконец, полагаем .

Множество всех термов, построенных из констант и функциональных символов, встречающихся в , называется эрбрановским универсумом для , а – его уровнем . Множества называются эрбрановскими множествами

Проиллюстрируем получение универсума Эрбрана на следующих примерах.

Пример 1. Пусть

Тогда

;

;

;

…………………………………….

.

Пример 2.

Пусть

Так как не существует никаких констант в , полагаем . Не существует никаких функциональных символов в , следовательно,

Пример 3.

Пусть .

Тогда
;

;

;

………………………………………………………

.

Пример 4.

Пусть ;

;

;

.

………………………………………………………

Если под выражением понимать терм, множество термов, атом, множество атомов, литеру, множество литер, дизъюнкт или множество дизъюнктов, то под фундаментальным выражением будем понимать выражение, в котором все переменные заменены элементами универсума Эрбрана. Так, фундаментальным примером дизъюнкта будем называть дизъюнкт, полученный заменой всех переменных в этом дизъюнкте элементами универсума Эрбрана таким образом, что все вхождения одной и той же переменной в дизъюнкт заменяются одним и тем же элементом универсума.

Множество фундаментальных атомов вида , где – все - местные предикатные символы, встречающиеся во множестве дизъюнктов и – элементы универсума Эрбрана, называется атомарным множеством или эрбрановской базой для . Обозначим эрбрановскую базу через .

Пример 5.

Пусть .

Тогда

Фундаментальные примеры: и т.п.

Определим теперь интерпретацию на универсуме Эрбрана и назовем ее - интерпретацией. Говорят, что интерпретация является - интерпретацией для множества дизъюнктов , если выполнены следующие соответствия:

- каждому предикатному символу соответствует некоторое - местное отношение в ;

- каждому функциональному символу соответствует некоторая - местная функция в (т.е. функция, отображающая в );

- каждой предметной константе из соответствует некоторая константа из (т.е. все константы отображаются на самих себя).

Пусть является эрбрановской базой для . Тогда - интерпретация может быть представлена множеством , в котором есть или для При этом, если есть то имеет значение “истина”, в противном случае “ложь”.

Пример 6. Пусть .

Тогда .

Примеры - интерпретаций:

;
;

При оба дизъюнкта выполнимы, при первый дизъюнкт выполним, второй нет, при оба дизъюнкта невыполнимы, т.е. принимают значение “ложь”.

В случае если интерпретация задана не на универсуме Эрбрана, а на произвольной области , то можно установить следующее соответствие между этими интерпретациями. Пусть дана интерпретация на некоторой области . Говорят, что - интерпретация соответствует интерпретации , если имеет место следующее: пусть – элементы и пусть каждый отображается на некоторый элемент области , тогда, если любой принимает значение “истина” (“ложь”) при интерпретации , то также принимает значение “истина” (“ложь”) при . Имеет место следующая теорема.

Теорема Множество дизъюнктов невыполнимо тогда и только тогда, когда ложно при всех - интерпретациях.

Доказательство «тогда» очевидно, а «только тогда» легко доказывается от противного введением соответствия между - интерпретацией и некоторой произвольной

интерпретацией. В дальнейшем будем рассматривать только

- интерпретации, и называть их просто интерпретациями .

Таким образом, для установления невыполнимости множества дизъюнктов необходимо и достаточно рассмотреть только - интерпретации.

Процедура вывода Эрбрана основывается на его теореме.

Теорема Эрбрана. Множество дизъюнктов невыполнимо тогда и только тогда, когда существует конечное невыполнимое множество фундаментальных примеров дизъюнктов .

Таким образом, для установления невыполнимости множества дизъюнктов необходимо образовать множества фундаментальных примеров дизъюнктов и последовательно проверять их на ложность. Теорема Эрбрана гарантирует, что, если множество дизъюнктов невыполнимо, то данная процедура обнаружит такое , что является ложным.

Процедура вывода Эрбрана состоит из двух этапов: сначала находится множество всех фундаментальных примеров дизъюнктов и затем, используя мультипликативный метод, из КНФ получают ДНФ.

Пример.

Пусть .

Находим

и фундаментальные примеры дизъюнктов:

.

Затем с помощью мультипликативного метода убеждаемся в невыполнимости .

£ Ú £ = £.

Недостаток процедуры вывода Эрбрана состоит в экспоненциальном росте множества фундаментальных примеров при увеличении . C помощью процедуры вывода Эрбрана удается доказать только простые теоремы.

Иной поход предложил Дж. Робинсон, который ввел принцип резолюции, являющийся теоретической базой для построения большинства методов автоматического доказательства теорем.

Дата добавления: 2015-06-27