Предваренная нормальная форма

Определение. Формула G имеет предваренную нормальную форму (сокращенно: ПНФ), если имеет следующий вид:

G=(Q₁,x₁)(Q₂,x₂)…(Q_n,x_n)H,

где Q₁,…,Q_n кванторы, а формула H не содержит кванторов.

Например, формула (x)(y)(P(x,y)&Q(y)) имеет предваренную нормальную форму, а формула (x)(T(x)&S(x,y)) не имеет.

Алгоритм приведения к предваренной нормальной форме

Шаг 1. Используя законы 1 и 2, исключить эквивалентность и импликацию:

1) F  G = (F  G) & (G  F)

2) F  G =F  G, G  F =G  F.

Шаг 2. Занести отрицание к атомарным формулам, пользуясь законами 15 – 17 и 29 – 30.

15) F = F

16) (F&G) = FG;

17) (FG) = F&G;

29) (x)F(x) = (x)F(x),

30) (x)F(x) = (x)F(x).

Шаг 3. С помощью законов 25 – 26, 31 – 36 вынести кванторы вперед, используя при необходимости переименование связанных переменных (законы 35 – 36):

25) (x)(F(x) G(x)) = (x)(F(x)  (x)G(x),

26) (x)(F(x)  G(x)) = (x)F(x)  (x)G(x).

31) (Qx)(F(x)  G) = (Qx)(F(x)  G), где G не содержит x,

32) (Qx)(F(x)  G) = (Qx)(F(x)  G), где G не содержит x.

33) (Q₁x)(Q₂y)(F(x)  G(y)) = (Q₁x)F(x)  (Q₂y)G(y),

34) (Q₁x)(Q₂y)(F(x) G(y)) = (Q₁x)F(x)  (Q₂y)G(y),

35) (x)F(x) = (y)F(y),

36) (x)F(x) = (y)F(y).

Рассмотрим пример: F = (x)P(x)  (y)(z)(P(y) & Q(y,z)).

Выполним шаг 1 (с помощью закона 2), получим формулу:

F₁=((x)P(x))  ((y)(z)(P(y) & Q(y,z))).

Выполним шаг 2 (с помощью закона 29), перейдем к формуле:

F₂=(x)P(x) (y)(z) (P(y) & Q(y,z)).

Выполним шаг 3 (закон 31 и 26 слева направо), получим формулу:

F₃=(x)(y) (P(x)(z)(P(y)Q(y,z))) и

F₄=(x)(y)(z)(P(x) (P(y) & Q(y, z))).

Пример.

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

Определение. Формула G имеет сколемовскую нормальную форму (сокращенно: СНФ), если имеет следующий вид:

G=(x)…(x_n)H,

где формула Н не содержит кванторов и имеет конъюнктивную нормальную форму.

Например, формула (x)[P(x)(P(y)&Q(x,y)] имеет сколемовскую нормальную форму, а формулы (x)(y)Q(x,y) и (x)[P(x)&(P(y)Q(x,y)] не имеют.

Алгоритм приведения к сколемовской нормальной форме

Шаг 1 – Шаг 3 – те же, что и в предыдущем алгоритме.

Шаг 4. Бескванторную часть привести к конъюнктивной нормальной форме, используя дистрибутивный закон № 7:

17) F(G&H) и (FG)&(FH).

Определение. Элементарной дизъюнкцией (или дизъюнктом) называется литера или дизъюнкция литер.

Определение. Формула G имеет конъюнктивную нормальную форму (сокращенно: КНФ), если она является элементарной дизъюнкцией или конъюнкцией элементарных дизъюнкций.

Например, формулы X,Y, XY, X&Y, (XY)&(XZ) имеют КНФ, а формулы XY, (XY), (X&Y)(X&Z) не имеют.

Если формула содержит формула вида: H₁(H₂&H₃), то можно заменить ее на равносильную ей формулу: (H₁H₂)&(H₁H₃) в соответствии с дистрибутивным законом № 7.

Шаг 5. Исключить кванторы существования. Используем следующие правила:

если левее удаляемого квантора существования нет ни одного квантора всеобщности, то переменная, относящаяся к этому квантору, заменяется символом константы, отличному от символов констант, уже имеющихся в H;

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

Символы констант и функциональные символы, которые используются для замены переменных, называются сколемовскими константами и функциями.

Например, формула (x) (y) (z) (u) P(x, y, z, u) в сколемовской стандартной форме имеет вид (y) (z) P(a, y, z, f(y, z)), т. е. кванторы существования удалены, а символы переменных x и u заменены на символ константы a и функциональный символ f(y, z).

Пусть имеется предваренная нормальная форма:

F₁=(x)(y) )(z)[P(x,y)(Q(x,z)R(y))].

Шаг 4. Бескванторную часть привести к конъюнктивной нормальной форме, используя дистрибутивный закон № 7:

F₂=(x)(y) )(z)[(P(x,y)Q(x,z))(P(x,y)(R(y))].

Шаг 5. Исключить кванторы существования. Сделаем подстановку x=a, z=f(y), получим искомую формулу:

G=(y)[(P(a,y)Q(a, f(y)))(P(a,y) R(y))].

Приведем пример приведения к СНФ. Пусть

F=(x)(y)[P(x,y)(z)(Q(x,z)R(y))].

Применяя законы 2 и 32, получаем формулу

F₁=(x)(y) )(z)[P(x,y)(Q(x,z)R(y))].

Она имеет предваренную нормальную форму. Используя закон 7 приводим бескванторную часть к КНФ:

F₂=(x)(y) )(z)[P(x,y)(Q(x,z)(P(x,y)(R(y))].

Сделаем подстановку x=a, z=f(y), получим искомую формулу

G=(y)[(P(a,y)Q(a, f(y)))(P(a,y) )R(y))].

Пример.

11