Эрбрановские интерпретации

Эрбрановские интерпретации были темой докторской диссертации Эрбрана в 1930 году. Несомненно, без вклада Эрбрана логическое программирование было бы до сих пор несбыточной мечтой. Основная проблема автоматического доказательства теорем состоит в построении универсальной процедуры, с помощью которой можно проверить, является ли данная формула логики предикатов общезначимой или нет. В 1936 г. Тьюринг и Чёрч независимо друг от друга доказали, что такой процедуры не существует. Однако Эрбран к этому времени уже решил косвенно эту проблему, предоставив алгоритм для построения интерпретации, опровергающей формулу j. Если формула j общезначима, опровергающей ее интерпретации не существует и алгоритм останавливается за конечное число шагов. В 1965 г. Робинсон, применяя метод Эрбрана, ввел и использовал понятие резолюции.

Определим, выполнимо ли предложение j. Ответ на вопрос о выполнимости предложения j получим, исследовав соответствующее ему множество дизъюнктов S. Интерпретация формул, образованных с помощью кванторов, требует определения логического значения находящейся в области действия квантора формулы при «пробегании» каждой переменной всей предметной области. Если предметная область является бесконечным множеством, задача становится невыполнимой.

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

Пусть сигнатура содержит функциональный символ f⁽ⁿ⁾ÎF, S – множество дизъюнктов, соответствующее предложению j. Опишем индуктивную процедуру построения эрбрановского универсума.

Шаг 1.

H₀={ c | константа с встречается в S} или , если S не содержит ни одной константы, где с₀ – новая константа (т.е. она не встречается в S), которая выбирается произвольно.

Шаг i+1.

H_i+1 определяется как множество всех термов, которые могут быть получены подстановкой в f⁽ⁿ⁾ всех термов, содержащихся в H_i.

H_i+1={f(a₁,…, a_n) | "j= a_j – термы из H_i, f⁽ⁿ⁾ÎF}.

Множества всех постоянных термов, входящих в H_i, i=0, 1, 2, …, называются эрбрановскими множествами для множества дизъюнктов S.

Эрбрановский универсум определяется как объединение множеств H_i, описанных выше: Все термы, образующие эрбрановский универсум, являются основными термами.

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

Примеры

1. Пусть задано множество дизъюнктов

где а – константа. Тогда H₀={ a }, H₁={ a, f(a)) }, H₂={ а, f(a), f(f(a)) }, …, H={ a, f(a), f(f(a)), f(f(f(a))),…} –множество основных термов.

2. Пусть теоретико-множественное представление " формулы имеет вид:

Так как среди аргументов термов отсутствуют константы, определяем H₀ введением константы a и получаем: H₀={ a }, H₁={ a, f(a,a), g(a) }, H₂={ a, f(a,a), g(a), f(g(a), g(a)), f(f(a,a), g(a)), f(g(a), f(a,a)), f(f(a,a),f(a,a)), g(f(a,a)),…}

3. Теоретико-множественное представление формулы имеет вид:

В множестве термов формулы отсутствуют константы. Для множества H₀ выбираем произвольную константу c ₀ из предметной области, H₀={c₀}. Так как в S не встречается ни одного функционального символа, эрбрановским универсумом для S является H=H₀={c₀}.

Примем без доказательства теорему Эрбрана: универсальное предложение j ("-формула, сколемовская нормальная форма), выполнимо (в какой-либо интерпретации) тогда и только тогда, когда оно выполнимо в эрбрановской интерпретации.

Следствие: если предложение j не выполнимо в эрбрановской интерпретации, то j не выполнимо, т.е. не существует интерпретации, в которой оно истинно.

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

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