Сколемовская нормальная форма

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

Пусть в модели M с предметной областью D предваренная нормальная форма для формулы Ф имеет вид

Ф «"x₁"x₂…"x_n$y₁$y₂…$y_mF(x₁,x₂,…,x_n,y₁,y₂,…,y_m).

Пусть для некоторого набора констант a₁,a₂,…,a_nÎD формула F выполнима. Это обозначается M╞($y₁$y₂...$y_m F(a₁,a₂,…,a_n,y₁,y₂,…,y_m)). Тогда значения переменных y_i, i= , при которых формула F выполнима в M, являются функциями от этого набора констант, т.е. "i= : y_i=j_i(a₁,a₂,…,a_n). Функции j_i(x₁,x₂,…,x_n) называются сколемовскими функциями.

Сколемовская нормальная форма (СНФ) является универсальным предложением, которое выполнимо тогда и только тогда, когда выполнима порождающая его формула, записанная в пренексной нормальной форме.

Для построения СНФ необходимо выполнить следующие действия:

1. Построить ПНФ предложения j.

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

В результате перехода к СНФ модель расширяется за счет появления новых функциональных символов.

Пример. Рассмотрим предложение j: $x"y"z$v P(x,y,z,v), которое находится в ПНФ.

Для построения сколемовской нормальной формы вычеркиваем квантор существования $x, заменяя вхождение переменной x на сколемовскую константу а, и квантор существования $v, заменяя переменную v на сколемовскую функцию f(z,y). Получаем предложение j1: "y"z P(a,y,z,f(z,y)).

Сколемовская функция f(z,y) указывает на существование переменной v, которая зависит от переменных z и y. Константа a означает сколемовскую функцию с арностью 0. Она замещает переменную x, связанную квантором существования, перед которым нет квантора общности.

Пример. Для формулы построить "-формулу. Для системы M=(N;<) найти требуемое обогащение.

Сколемовская нормальная форма для записанной формулы имеет вид:

Полученная формула выполнима в модели M1= (N;<;j₁(x), j₂(x,y)), если j₁(x)=x+1, j₂(x,y)=x.

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

Как и в логике высказываний, в логике предикатов имеется возможность теоретико-множественного представления "-формул. Поскольку в "-формуле все свободно входящие переменные связаны кванторами общности, формула выполнима тогда и только тогда, когда подформула, находящаяся в области действия кванторной приставки, является тавтологией, т.е. тождественно истинной в любой интерпретации и в произвольной предметной области. Эта формула называется матрицей, если она представлена в КНФ, т.е. в виде конъюнкции дизъюнктов произвольных рангов. Элементами дизъюнктов являются атомы (предикатные символы из множества предикатных символов R) с отрицаниями или без.

Литерал – это атом или его отрицание. Дизъюнкт – это дизъюнкция литералов.

Теоретико-множественное представление формулы – это множество, мощность которого равна числу сомножителей КНФ. Его элементами являются множества литералов каждого из дизъюнктов, составляющих КНФ.

Пусть предложение j: "x₁,…, "x_l A(x₁,…, x_l), - формула логики предикатов, где бескванторная формула А представлена в КНФ вида C₁(x₁,…, x_l)&…&C_k(x₁,…, x_l), где дизъюнкция литералов. Теоретико-множественным представлениемпредложения j является множество

S={C₁,…, C_k}={{P_i1,…, P_in},…, {P_k1,…, P_kn}}.

Здесь P_ij – атомы, входящие в дизъюнкт C_j.

Например, для предложения "x"z[A(x,y)&(B(x)ÚC(z))&D(z,x)] теоретико-множественное представление имеет вид:

S={{A(x,y)}, {B(x), C(z)}, {D(z,x}}}.