13.2. Предваренные нормальные формы

Определение 13.1. Формула А находится в предваренной нормальной форме (ПНФ), если она имеет вид: (Q₁x₁)…(Q_nx_n)M, где каждое Q_ix_i. есть х_i или x_i, а М — формула в конъюнктивной нормальной форме, не содержащая кванторов. (Q₁x₁)…(Q_nx_n) называется префиксом, а М — матрицей формулы А.

Теорема 13.1. Существует эффективная процедура приведения любой формулы логики предикатов к эквивалентной ей пред­варенной нормальной форме.

Доказательство теоремы конструктивно, т.е. дает алгоритм пре­образования любой формулы к предваренной нормальной форме. Теорема доказывается индукцией по числу связок т.

1. Пусть m = 0. Тогда формула А не содержит связок и находится в ПНФ.

2. Предположим, что существует ПНФ для формулы В с числом связок п. Докажем, что существует ПНФ для формулы А с числом связок m = n + 1.

1 случай. Пусть существует ПНФ для В=(Q₁x₁)…(Q_nx_n)M. Формула А образована из В с помощью операции отрицания: А=(Q₁x₁)…(Q_nx_n)M. По законам де Моргана связка _­ проносится через кванторы: xM  xM, xM  xM. Полученная фор­мула будет находиться в ПНФ.

2 случай. Формула А образована из двух формул В1 и В2 с числом связок n < m с помощью связок конъюнкции & или дизъюнкции :

(Q₁x₁)…(Q_nx_n)M1  (Q₁y₁)…(Q_ny_n)M2

Тогда, если формулы В1 и В2 имеют кванторы по одной и той же переменной, используем законы замены связанных переменных:

xP(x)  yP(y), xP(x)  yP(y),

так, чтобы ни одна свободная переменная не стала связанной в результате этой замены. После этого воспользуемся законами ком­мутативности для & и  и законами пронесения кванторов:

x(P(x)B)  xP(x)B, x(P(x)B)  xP(x)B,

x(P(x)B)  xP(x)B, x(P(x)B)  xP(x)B,

(В не содержит вхождений x).

3 случай. Формула А образована из В навешиванием квантора  или . Тогда, поскольку В находится в ПНФ, вновь полученная формула будет в ПНФ.

Примеры.

1. Приведем к ПНФ следующую формулу:

хР(х)х(уD(у)&L(х, у)) = хP(х)х(уD(у)&L(х, у)) =

= хР(х)х(уD(у)&L(х, у)) = хP(х)z(уD(у)&L(z, у)) =

= х(Р(х)z(уD(у)&L(z, у))) = х(z(уD(у)&L(z, у))Р(х)) =

= хz(vD(v)&L(z, у))Р(х) = хzv((D(v)&L(z, у))Р(х)) =

= хzv((D(v)Р(х))&(L(z, у))Р(х))

2. Рассмотрим посылки примера 12.1.

х(Р(х)&y(D(у)L(х, у))) = х(Р(х)&y(D(у)L(х, у))) =

= х(y((D(у)L(х, у))&Р(х)) = хy((D(у)L(х, у))&Р(х)).

х(Р(х)y(Q(у)L(х, у))) = х(Р(х)y(Q(у)L(х, у))) =

= х(y(Q(у)L(х, у))Р(х)) = хy(Q(у)L(х, у)Р(х)).

13.3. Скулемовские стандартные формы

Определение 13.2. Предваренная нормальная форма, содержа­щая только кванторы всеобщности, называется скулемовской стандартной формой (ССФ).

Процедура приведения ПНФ к скулемовской форме заключа­ется в элиминации (удалении) кванторов существования.

Пусть формула А находится в предваренной нормальной форме (Q₂x₂)…(Q_nx_n)M, где М есть конъюнктивная нормальная форма. Если квантор существования – первый слева квантор в префиксе: (x₁)(Q₂x₂)…(Q_nx_n)M, то его можно элиминировать на основании правила экзистенциальной конкретизации. Выберем константу с, отличную от других констант, входящих в М, заменим все вхождения x₁, встречающиеся в М, на с, и вычеркнем квантор x₁ из префикса.

Если же перед квантором существования стоит квантор всеобщ­ности, например, хуМ, то переменная у попадает в область дей­ствия квантора всеобщности, и выражение ху (для каждого х существует у) означает наличие некоторой функциональной зависимости у =f(x). Если квантору существования предшествует несколько кванторов всеобщности, то функция зависит от всех переменных, по которым навешены эти кванторы. В общем случае, если Qs₁, …, Qs_m – список всех кванторов всеобщности, встречаю­щихся левее х_r, 1  s₁ < s₂ < ... < s_m < r, мы выберем m-местный функциональный символ f, отличный от других функциональных символов, заменим все х_r в М на f(х_s1, ..., х_sm) и вычеркнем х_r из префикса. Затем весь этот процесс применим для всех кванторов существования в префиксе; последняя из полученных формул есть скулемовская стандартная форма — для краткости, стандартная форма (ССФ) формулы А. Функции, используемые для замены переменных квантора существования, называются скулемовскими функциями (константы есть нульместные функции).

Пример. Получим стандартную форму формулы А = xyzuvwP(x, y, z, u, v, w). В этой формуле левее х нет никаких кванторов всеобщности, левее u стоят у и z, а левее w стоят у,z и v Следовательно, мы заменим переменную х на константу а, переменную u – на двуместную функцию f(у, z), переменную w – на трехместную функцию g(у, z, v). Таким образом, мы получаем следующую стандартную форму формулы

А: S=yzvP(a, y, z, f(y, z), v, g(y, z, v)).

Для рассмотренных выше посылок из примера 12.1 ССФ имеет вил:

ху((D(y)L(x, y))&P(x))у((D(y)L(a, y))&P(a)), xу(Q(y)L(x, y)P(x)).

Если предваренная нормальная форма эквивалентна исходной формуле, то скулемовская стандартная форма формулы A, вообще говоря, не эквивалентна ей. Например, пусть А=хР(х) и S=P(а) есть стандартная форма формулы А. Пусть I есть следующая интерпретация: область D={а, b}, Р(а)=F, P(b)=T. Тогда A истинна в I, но S ложна в I. Таким образом, А не эквивалентна S. Однако, если Р(а)=F, P(b)=F, то |A|=F, и S=P(a) – также принимает значение F для любого a. Таким образом, AS в том и только том случае, если А противоречива. Докажем, что это действи­тельно так.

Теорема 13.2. Пусть S – стандартная форма формулы A. Тогда A противоречива в том и только том случае, когда S проти­воречива.

Доказательство. Пусть формула А находится в ПНФ, т.е. A=(Q₁x₁)…(Q_nx_n)M[x₁, …, x_n]. (Запись М[х₁, ..., х_n) означает, что матрица М содержит переменные х₁, ..., х_n). Пусть Q_r - первый слева квантор существования.

Пусть A₁=(x₁)…( x_r-1)(Q_r+1x_r+1)...(Q_nx_n)M[x₁,…,x_r-1, f(x₁,…,x_r-1), x_r+1,…,x_n], где f – скулемовская функция, соответствующая x_r, 1rn. Мы хотим показать, что A противоречива тогда и только тогда, когда A, противоречива. Предположим, что A противоречива. Если A₁ непротиворечива, то существует такая интерпретация I, что A₁ истинна в I. т.е. для всех x₁,...,x_r-1 существует по крайней мере один элемент f(х₁,..., х_r-1), для которого (Q_r+1x_r+1)...(Q_nx_n)* *M[x₁,…,x_r-1, f(x₁,…,x_r-1), x_r+1,…,x_n] истинна в I. Таким образом, A истинна в I, что противоречит предпо­ложению, что A противоречива. Следовательно, A₁ должна быть противоречива. С другой стороны, предположим, что A₁ противоре­чива. Если А непротиворечива, то существует такая интерпретация I на области D, что A истинна в I, т.е. для всех x₁,…,x_r-1, существует такой элемент х_r, что (Q_r+1x_r+1)...(Q_nx_n)M[x₁,…,x_r-1, f(x₁,…,x_r-1), x_r+1,…,x_n] истинна в I. Расширим интерпретацию I, включив в нее функцию f(x₁,…,x_r-1)=х_r, которая отображает (x₁,…,x_r-1) на х_r для всех x₁,…,x_r-1 в D, Обозначим это расширение I. Тогда для всех x₁,…,x_r-1 (Q_r+1x_r+1)...(Q_nx_n)* *M[x₁,…,x_r-1, f(x₁,…,x_r-1), x_r+1,…,x_n] истинна в I, т.е. A, истинна в I, что противоречит предположению, что A­₁ противоречива. Следовательно, А должна быть противоречивой. Предположим теперь, что в A имеется m кванторов существования. Пусть А₀=А. Пусть А_k получается из А_k-1 .заменой первого квантора существования в А_k-1 , скулемовской функцией, k-1,…,m. Тогда стандартная форма S=A_m. Используя те же рассуждения, что были даны выше, мы можем показать, что А_k-1 противоречива тогда и только тогда, когда А_k противоречива при k = 1,...,m. Следовательно, А противоречива тогда и только тогда, когда S противоречива, что и требовалось доказать.

Определение 13.3. Предикатные буквы будем называть литерами. Дизъюнкция литер называется дизъюнктом, или клаузой (сlаusе) (иногда клозом). Однолитерный дизъюнкт называется единичным дизъюнктом. Когда дизъюнкт не содержит никаких литер, его называют пустым дизъюнктом. Так как пустой дизъюнкт не содержит литер, которые могли бы быть истинными при любых интерпретациях, то пустой дизъюнкт всегда ложен. Пустой дизъюнкт обозначается символом 

Пусть S — стандартная форма формулы А. Матрица формулы, представленной в ССФ. находится в конъюнктивной нормальной форме, т.е. в виде конъюнкции дизъюнктов. Будем представлять ССФ формулы А множеством дизъюнктов, где каждая переменная считается управляемой квантором всеобщности. Множество дизъ­юнктов – это просто другая форма представления стандартной формы формулы А, поэтому в дальнейшем будем обозначать его так же, как и ССФ — символом S. Считаем, что множество дизъюнк­тов S есть конъюнкция всех дизъюнктов из S. Например, ССФ посылки из примера 12.1: y((D(у)L(a, у))&P(a)) может быть представлена множеством дизъюнктов: S={D(у)L(a, у), P(a)}.

Далее, если мы имеем А=А₁& ...&А_n, мы можем отдельно получить множества дизъюнктов S_i, i=1, …, n, где каждое S­i представляет стандартную форму А_i. Затем пусть S=S₁…S_n. Тогда А противоречива тогда и только тогда, когда S противоречиво. Говорят, что множество дизъюнктов невыполнимо, если соответству­ющая стандартная форма противоречива, и выполнимо в противном случае.