В исчислении предикатов не существует универсального алгоритма, который позволяет проверить общезначимость, нейтральность, невыполнимость формулы, т.к. для формулы исчисления предикатов существует бесконечное число интерпретаций. Однако было установлено, что множество дизъюнктов (СНФ) невыполнимо тогда и только тогда, когда принимает значение ложь на всех интерпретациях, на любых областях. Но так как рассмотрение всех интерпретаций на любых областях невозможно, хорошо было бы найти такую специальную область интерпретации, установив на которой факт невыполнимости множества дизъюнктов, можно было бы сделать вывод о невыполнимости этого множества на любых других областях интерпретаций. Такая область существует, называется универсумом Эрбрана и определяется следующим образом.
Пусть Hо – множество констант, появляющихся в множестве дизъюнктов S. Если в S нет констант, то в Hо включается некоторая константа, например Hо = {a}. Для i = 0,1,2, … Hi+1 = Hi È {fn(t1, t2, …, tn)}, где fn – все n-местные функциональные символы, встречающиеся в S, а t1, t2, …, tn – элементы множества Hi.
Тогда множество H = H¥ называется универсумом Эрбрана для S, а Hi – его уровнем i. Элементы эрбрановой области не имеют конкретных значений, это синтаксические объекты.
Пример. Пусть S = { P(x, a, g(y)) Ú ¬Q(х)), ¬P(f(x), a, y) Ú Q(a)}. Тогда
Ho = {a};
H1 = {a, f(a), g(a)};
H2 = {a, f(a), g(a), f(f(a)), f(g(a)), g(f(a)), g(g(a))};
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
H¥ = {a, f(a), g(a), f(f(a)), f(g(a)), …}.
На универсуме Эрбрана вводится понятие эрбрановой интерпретации, или H-интерпретации. Говорят, что интерпретация IH является H-интерпретацией для множества дизъюнктов S, если выполнены следующие условия:
1) каждому предикатному символу Pjn соответствует некоторое n-местное отношение в H;
2) каждому функциональному символу fjn соответствует некоторая n-местная операция в H ( т. е. функция, отображающая Hn в H);
3) каждой предметной константе ai из S соответствует некоторая константа из H (т. е. все константы отображаются на самих в себя).
Пример. Пусть S = {¬P(f(x)) Ú Q(x), R(x)}. Тогда примеры H-интерпретаций следующие:
I1H = {P(a), Q(a), R(a), P(f(a)), Q(f(a)), R(f(a)), …}.
I2H = {¬P(a), ¬Q(a), ¬R(a), ¬P(f(a)), ¬Q(f(a)), ¬R(f(a)), …}.
I3H = {P(a), ¬Q(a), ¬R(a), P(f(a)), ¬Q(f(a)), ¬R(f(a)), …}.
При I1H оба дизъюнкта выполнимы, при I2H первый дизъюнкт выполним, второй – нет, при I3H оба дизъюнкта невыполнимы, т. е. принимают значение «ложь».
В случае, если интерпретация задана не на универсуме Эрбрана, а на произвольной области D, то можно установить следующее соответствие между этими интерпретациями. Пусть дана интерпретация I на некоторой области D. Говорят, что H-интерпретация IH соответствует интерпретации I, если имеет место следующее: пусть h1, h2, …, hn, … – элементы H и пусть каждый hi отображается на некоторый элемент di области D, тогда если любой P(d1, d2, …, dn) принимает значение «истина» («ложь») при интерпретации I, то P(h1, h2, …, hn) также принимает значение «истина» («ложь») при IH.
Справедлива следующая теорема: множество дизъюнктов S невыполнимо тогда и только тогда, когда S ложно при всех H-интерпретациях. Таким образом, для установления невыполнимости множества дизъюнктов достаточно рассмотреть не все его интерпретации, а только H-интерпретации.
Процедура вывода Эрбрана основывается на его теореме, которая гласит: множество дизъюнктов S невыполнимо тогда и только тогда, когда существует конечное невыполнимое множество фундаментальных примеров дизъюнктов в S.
Фундаментальным примером дизъюнкта называется дизъюнкт, полученный заменой всех переменных в этом дизъюнкте элементами универсума Эрбрана таким образом, что все вхождения одной и той же переменной в дизъюнкт заменяются на один и тот же элемент универсума.
Таким образом, для установления невыполнимости множества дизъюнктов необходимо образовать множества S1, S2, …, Sn, … фундаментальных примеров дизъюнктов и последовательно проверить их на ложность. Теорема Эрбрана гарантирует, что если множество S невыполнимо, то данная процедура обнаружит такое n , что Sn является ложным.
Недостаток процедуры Эрбрана состоит в экспоненциальном росте множеств Si при увеличении i. Иной подход предложил Дж. Робинсон, который ввел принцип резолюций, являющийся теоретической основой для построения большинства методов автоматического доказательства теорем.