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

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

Тьюринг, Черчь. Доказали, что такой универсальной процедуры не существует.

Эрбран. Предложил алгоритм построения интерпретации (эрбрановской интерпретации), опровергающей формулу . Если  - общезначима, то опровергающей интерпретации не существует, и алгоритм в этом случае останавливается через конечное число шагов.

Эрбрановский универсум предложения 

ЭУ - это множество объектов (область определения эрбрановской интерпретации), на котором принимают значения термы предложения .

Алгоритм (построения эрбрановского универсума) Пусть  - предложение PrL и S – соответствующее  множество дизъюнктов. Итерационная схема:

1. H₀={c | где c – константа из множества S}

2. H₀={c₀}, если S не содержит констант. c₀ – новая константа, выбирается произвольным образом.

3. Пусть построено множество H_i

H_i+1=H_i U {f(t₁, … , t_n) | t_i, i=1..n – термы из H_i; f() – функция из S}

Множество H=H₀ U H₁ U … U H_i U … называется эрбрановским универсумом.

Пример. Рассмотрим множество дизъюнктов S={{P(a)}, {P(a), R(g(x))}}, здесь a – const

H₀={a}

H₁={a, g(a)}

H₂={a, g(a), g(g(a))}

…

H={a, g(a), g(g(a)), g(g(g(a))), …}

Пример. S={{Q(f(x),g(x))}, {P(x)}}. Требуется построить множества H₀, H₁, H₂, H₃

H₀={a} Здесь a – новая константа

H₁={a, f(a), g(a)}

H₂={ 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)), g(f(a)), g(g(a)), f(f(f(a))), f(f(g(a))), f(g(f(a))), f(g(g(a))), g(f(f(a))), g(f(g(a))), g(g(f(a))), g(g(g(a)))}

…

Пример. S={{Q(x),P(x)}}. Требуется построить эрбрановский универсум

H₀={a}, a – новая константа

H={a} (Эрбрановский универсум)

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

Определение (Эрбрановской интепретации) Пусть S – множество дизъюнктов, H – эрбрановский универсум, соответствующий S. Множество _H называется эрбрановской интерпретацией для S, если

_H={A, (R₀), (R₁), … , (f₀), (f₁), … , (c₀), (c₁), …}, где

• A=H – эрбрановский универсум (область интерпретации)

• (c_k) = c_k – (интерпретация константы)

• (f_j)((t₁),…,(t_m)) = f_j((t₁),…,(t_m)) – m-местная функция, где (t_i) – интерпретация терма t_i (интерпретация функционального символа)

• (R_i)((t₁),…,(t_n)) = R_i((t₁),…,(t_n)) – n-местное отношение, где (t_i) – интерпретация терма t_i (интерпретация предиката)

Теорема (об эрбрановских интерпретация) Пусть  - универсальное предложение (в СНФ) и S – соответствующее множество дизъюнктов. Предложение  выполнимо (истинно в некоторой интерпретации) тогда и только тогда, если  выполнимо в эрбрановской интерпретации.

Замечание. Если  невыполнимо в эрбрановской интерпретации, то не существует интерпретации, в которой  истинно.

5. Метод семантических деревьев

Пусть  - предложение PrL и S={₁,…,_n} – соответствующее  множество дизъюнктов.

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

По теореме об эрбрановских интерпретациях: если  выполнимо в некоторой интерпретации, то  истинно и в эрбрановской интерпретации. Для того чтобы предложение  было истинно в эрбрановской интерпретации, достаточно, чтобы были истинны в эрбрановской интерпретации все основные примеры дизъюнктов   S.

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

Метод семантических деревьев – регулярная процедура построения всех основных примеров дизъюнктов. Если  невыполнимо, то на некотором шаге метода будет построено множество основных примеров дизъюнктов   S, опровергающих .

Основной пример атома (в методе семантических деревьев)

Пусть  - универсальное предложение и S={С₁,…,С_n} – соответствующее  множество дизъюнктов.

• Пусть P₁(),…,P_k() – атомы (предикаты), входящие в дизъюнкты множества S.

• H={a₁, a_2, … } – эрбрановский универсум для S.

Тогда P_l(a_i, … , a_k) – основной пример атома.

Пример 1. Рассмотрим предложение

: (x)[P(x)  (P(x)  Q(f(x)))  (Q(f(x))]

Множество дизъюнктов имеет вид:

S={{P(x)},{P(x),Q(f(x))},{Q(f(x)}}

Эрбрановский универсум H:

H={a, f(a), f(f(a)), f(f(f(a))), …}

Основные примеры атомов [P(.), Q(f(.))]:

{P(a), P(f(a)), Q(f(a)), Q(f(f(a))), P(f(f(a))), Q(f(f(f(a)))), … }

Определение семантического дерева

Пусть  - универсальное предложение и S={С₁,…,С_n} – соответствующее  множество дизъюнктов.

• Пусть P₁(),…,P_k() – атомы (предикаты), входящие в дизъюнкты множества S.

• H={a₁, a_2, … } – эрбрановский универсум для S.

Семантическим деревом для S называется дерево T со следующими свойствами:

1. Корнем T является произвольная точка.

2. Вершиной T является основной пример атома P_l(a_i, … , a_k) или его отрицание P_l(a_i, … , a_k)

3. Потомки. Каждая вершина имеет в точности двух потомков: P_l(a_i, … , a_k) и P_l(a_i, … , a_k)

4. Построение дерева. Дерево T строится, начиная от корня. К каждой вершине, не имеющей потомков, добавляется два новых узла, в которых размещается очередной основной пример атома P_l(a_i, … , a_k) и его отрицание P_l(a_i, … , a_k).

5. Ветвь, содержащая в вершинах основные примеры атомов или отрицаний атомов, трактуется как конъюнкция основных примеров атомов вершин.

6. Если вершина дерева сдержит основной пример атома P_l(a_i, … , a_k), то ни одна ветвь, проходящая через эту вершину, не может содержать узел P_l(a_i, … , a_k).

7. Противоречивая ветвь (a). Если в процессе построения дерева T получена вершина k (основной пример атома), которая противоречит какому-либо основному примеру одного из дизъюнктов С₁,…,С_n, тогда k является заключительной вершиной и текущая ветвь является противоречивой .

8. Противоречивая ветвь (b). Если конъюнкция основных примеров атомов на некоторой ветви противоречит какому-либо основному примеру одного из дизъюнктов С₁,…,С_n, то текущая ветвь также является противоречивой 

9. Непротиворечивая ветвь. Каждой непротиворечивой ветви дерева T соответствует эрбрановская интерпретация, подтверждающая исходное множество дизъюнктов.

10. Все ветви противоречивы. Если для множества дизъюнктов S существует семантическое дерево T, все ветви которого противоречивы, то множество дизъюнктов S является противоречивым.

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

Пример 1 (продолжение). Требуется проверить выполнимость следующего предложения:

: (x)[P(x)  (P(x)  Q(f(x)))  (Q(f(x))]

Соответствующее множество дизъюнктов имеет вид:

S={{P(x)},{P(x),Q(f(x))},{Q(f(x)}}

Эрбрановский универсум H:

H={a, f(a), f(f(a)), f(f(f(a))), …}

Основные примеры атомов [P(.), Q(f(.))]:

{P(a), P(f(a)), Q(f(a)), Q(f(f(a))), P(f(f(a))), Q(f(f(f(a)))), … }

Построение семантического дерева T



1

P(a)

P(a)

{P(a)}

)





2

P(a)

P(a)

{P(a)}

)



P(f(a))

{P(f(a))}

P(f(a))





3

P(a)

P(a)

{P(a)}

)



P(f(a))

{P(f(a))}

P(f(a))

Q(f(a))

{Q(f(a))}



Q(f(a))





{P(a),Q(f(a))}

[P(a)  Q(f(a))]  [P(a)  Q(f(a))]

Выводы. Все ветви дерева T противоречивы, следовательно, не существует эрбрановской интерпретации, подтверждающей множество дизъюнктов

S={{P(x)},{P(x),Q(f(x))},{Q(f(x)}}

Невыполнимое множество основных примеров дизъюнктов (в это множество включаются только те основные примеры дизъюнктов, которые были использованы для объявления некоторой ветви противоречивой) имеет вид:

S’={{P(a)}, {P(f(a))}, {Q(f(a))}, {P(a),Q(f(a))}}

т.е. следующая формула неподтверждаема:

P(a)  P(f(a))  [Q(f(a))]  [P(a)  Q(f(a))]

Пример 2. Требуется проверить выполнимость следующего предложения:

: (x)(y) [P(x,y)  P(a,f(x,y))]

Соответствующее множество дизъюнктов имеет вид:

S={{P(x,y), P(a,f(x,y))}}

Эрбрановский универсум H:

H={a, f(a,a), f(a,f(a,a)), f(f(a,a),a), …}

Основные примеры атомов [P(.,.), P(a, f(.,.))]:

{P(a,a), P(a,f(a,a)), P(f(a,a),a), P(f(a,a), f(a,a)), … }

Построение семантического дерева T



1

P(a,a)

P(a,a)

)



2

P(a,a)

P(a,a)

)

P(a,f(a,a))

P(a,f(a,a))

P(a,f(a,a))

P(a,f(a,a))

P(f(a,a),a)



P(f(a,a),a)

P(f(a,a),a)

P(f(a,a),a)

…

…

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

Задание 6. Методом семантических таблиц требуется проверить выполнимость следующего предложения:

: (x)(z) [(P(x)  Q(f(x),x))  P(g(b))  Q(x,z)]

Здесь b – константа, f(), g() – функциональные символы, P(), Q() - предикаты. Если предложение  невыполнимо, нужно построить невыполнимое множество основных примеров дизъюнктов.

12