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

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

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

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

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

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

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

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

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

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

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

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

j: ("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)))), … }