Н-интерпретации

Алгоритмическая неразрешимость проблемы проверки общезначимости формул в ИП в общем случае, следующая из теоремы Чёрча, не означает полную бесперспективность применения к анализу формул ИП универсальных разреша-ющих алгоритмов. Проблема заключается в том, что в слу-чае применения таких алгоритмов к произвольной формуле А могут возникнуть три возможных ситуации:

а) алгоритм подтверждает общезначимость А,

б) алгоритм работает теоретически бесконечно долго при наличии общезначимости у А,

в) алгоритм работает теоретически бесконечно долго при наличии невыполнимости А.

В первом случае алгоритм решает задачу, во втором и третьем - нет.

Начало конструированию разрешающих алгоритмов было положено Эрбраном, который предложил в 30-х годах ХХ века теоретически правильный алгоритм построения ин-терпретаций, опровергающих рассматриваемую формулу. В нем доказательство общезначимости формулы А сводится к доказательству невыполнимости ее отрицания В=Ø А. Основная идея алгоритма заключается в том, что невыпол-нимость формулы В, заменённой матрицей скулемовской формы, проверяется на одной специальной предметной области - эрбрановском универсуме, который строится по В и описывает все возможные варианты значений термов, которые могут входить в неё (с точностью до обозначений). Поскольку такие области в большинстве случаев бесконеч-ны, то проверку общезначимости формул на них алгоритм теоретически никогда бы не закончил. Проверка невыпол-нимости (если таковая имеет место) теоретически должна

заканчиваться за конечное число шагов.

Матрица скулемовской формы является конъюнкцией дизъюнктов вида:

M = D₁ & D₂ &... &D_k .

Очевидно, матрица М опровержима (невыполнима) тогда и только тогда, когда на любой интерпретации I опровержим хотя бы один из дизъюнктов D_i , входящих в неё.

Обозначим множество дизъюнктов, входящих в мат-рицу, через S: S = {D₁ , D₂ ,...,D _k }.

Обозначим множество всех констант, входящих в S, через {С_S}. Множество символов функциональных пере-менных, входящих в S, - через { F_S}.

Эрбрановский универсум, соответствующий множест-ву дизъюнктов S, обозначим через H(S). Он строится сле-дующим образом:

0. Множество нулевого уровня H₀={С_S}.

1. Через F_S (H₀) обозначим результат всех возможных под-становок констант, содержащихся в H₀, в функции из {F_S}. Множество первого уровня H₁ = H₀ È F_S (H₀ ).

...

i. F_S (H_i-1 ) - результат всех возможных подстановок кон-стант из H_i-1 в функции из {F_S }. Множество i-го уровня H_i = H_i-1 È F_S (H_i-1 ).

В пределе получаем: H(S) = H_¥.

Эрбрановский универсум как бы моделирует все воз-можные значения термов, входящие в S (с точностью до обозначений).

Пример 1. Построить эрбрановский универсум H(S), соответствующий множеству дизъюнктов S = {P(a),ØP(x)}.

Решение. {С_S}= {а}, { F_S}= {Æ}. H₀={С_S}= {а}, так как {F_S} = {Æ}, то H₀ = H₁ =... = H_¥ = {а}.

Пример 2. Построить эрбрановский универсум H(S), соответствующий множеству дизъюнктов S = {P(a), P(x) Ú Q(f(x))}.

Решение. {С_S}= {а}, { F_S}= {f}.

1. H₀={С_S}= {а}.

2. F_S (H₀ ) = {f(a)}. H₁ = {a}È {f(a)}= {a, f(a)}.

3. F_S (H₁ ) = {f(a), f(f(a))}. H₂ = {a, f(a)}È {f(a), f(f(a))} = {a, f(a), f(f(a))}.