4.6. Упрощение формул

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

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

Формула Q₁y₁Q₂y₂ … Q_ny_n , где – Q_i кванторы, а  не имеет кванторов, называется пренексной (или предваренной) нормальной формой. Существует эффективная процедура приведения формулы к пренексной нормальной форме. Она основана на следующих далее правилах преобразования, вытекающих из логических аксиом исчисления предикатов.

Обозначим  = ,  = . Имеет место эквивалентность формул Qx  Qx. При условии, что переменная х не входит свободно в формулу , верны равенства:

1) Qx &   Qx( & );

2) Qx    Qx(  );

3) (  Qx)  Qx(  );

4) (Qx  )  Qx(  );

Имеет место эквивалентность формул:

5) Qx  Qy(x/y)

Пример 1

Найдём пренексную нормальную форму формулы x  , где  и  не содержат кванторов, и х не входит свободно в . Представим её как

(x  ) & (  x).

С помощью равенств 3 – 4 она приводится к виду:

x(  ) & x(  ).

С помощью равенства 1 – к виду: x((  ) & x(  )).

С помощью равенства 5 – к виду: x((  ) & y(  (y/x))),

где y не входит в преобразуемую формулу. Снова из равенства 1 получаем:

xy((  ) & (  (y/x))).

Элиминация кванторов

По пренексной нормальной форме  строится формула *, не содержащая кванторов. Кванторы всеобщности удаляются, а кванторы существования заменяются на функциональные символы, добавляемые к языку:

y(y, x₁, …, x_n) переходит в (f(x₁, …, x_n), x₁, …, x_n), и операция f добавляется к языку.

Пример 2

Пусть  x₁ x₂ x₃ x₄ x₅ x₆ (x₁, x₂, x₃, x₄, x₅, x₆). Выполним действия для приведения к бескванторной форме:

1) удалим x₁ и заменим x₁ константой b₁:

x₂ x₃ x₄ x₅ x₆ (b₁, x₂, x₃, x₄, x₅, x₆);

2) удалим два квантора всеобщности:

x₄ x₅ x₆ (b₁, x₂, x₃, x₄, x₅, x₆);

3) удалим квантор существования и к L добавим символ операции x₄ = f(x₂, x₃):

x₅ x₆ (b₁, x₂, x₃, f(x₂, x₃), x₅, x₆);

4) удалим квантор существования и к L добавим символ операции x₅ = g(x₂, x₃):

x₆ (b₁, x₂, x₃, f(x₂, x₃), g(x₂, x₃), x₆);

5) удалим квантор всеобщности:

 = (b₁, x₂, x₃, f(x₂, x₃), g(x₂, x₃), x₆).

Полученная формула определена в языке L = L  {b₁, f, g}.

Пусть  – множество предложений в языке L. Обозначим через  формулу, полученную из предложения  приведением к пренексной нормальной форме с последующей элиминацией кванторов и преобразованием языка L. Положим . Пусть в результате преобразований формул    в  мы пришли к расширенному языку L.

Теорема (вторая -теорема)

а) Если  – формула языка L, то вывод   существует тогда и только тогда в L, когда существует вывод   в L

б) Теория  непротиворечива, если и только если непротиворечива теория .

4.7. Метод резолюций Робинсона

В предыдущем разделе мы научились приводить формулы к виду, пригодному для применения метода автоматического доказательства теорем, предложенного в 1965 году Робинсоном.

Задача ставится так: заданы язык первого порядка L и конечное множество аксиом . Требуется найти вывод   для произвольной формулы .

Она решается методом резолюций. Идею этого метода продемонстрируем сначала для случая, когда L – исчисление высказываний с множеством пропозициональных символов Р. Напомним, что для каждого символа А  Р символы А и А называются литералами. Клоусом, или дизъюнктом называется дизъюнкция литералов .

Если D₁ и D₂ – дизъюнкты, для которых существуют такие дизъюнкты и литерал В, что и , то формула:

называется резольвентой D₁ и D₂.

Предположим, что требуется доказать вывод ₁, ₂, …, _n . Сведём задачу к доказательству противоречивости формулы ₁ & ₂ & …& _n & . Приведём последнюю к конъюнктивной нормальной форме. Получим конъюнкцию некоторых дизъюнктов, составляющих список:

D₁, D₂, …, D_k.

Далее в цикле перебираем пары дизъюнктов из этого списка, находим резольвенты и добавляем эти резольвенты, которые, очевидно, будут дизъюнктами, в конец списка. Если в списке появится 0, то вывод доказан. Если новые дизъюнкты не могут быть построены, то вывода нет.

Пример 1

Пусть требуется установить выводимость a  b a  c  b  c. Перенесём левую часть вправо, получим формулу: (a  b)  (a  c)  b  c, которую надо доказать. Будем доказывать противоречивость конъюнкции дизъюнктов:

a  b, a  c, b, c.

Так как , то к списку добавляется дизъюнкт b  c. Затем добавим . Получим список:

a  b, a  c, b, c, b  c, с.

Теперь Res (c, с) = 0 даёт противоречие. Значит, выводимость имеет место.

Рассмотрим теперь метод резолюций для нахождения вывода в исчислении предикатов. Мы видели, что можно предполагать формулы  и аксиомы из , не имеющими кванторов. Для любых двух атомных формул Р(s₁, …, s_m) и Q(t₁, …, t_n) их наибольший общий унификатор  определён, если и только если P = Q, m = n, и система уравнений s₁ = t₁, s₂ = t₂, …, s_n = t_n унифицируема. Литералами в исчислении предикатов называются атомные формулы и их отрицания. Дизъюнкт определяется как дизъюнкция литералов. Два дизъюнкта D₁ и D₂ называются резольвируемыми, если существуют литералы B₁ и B₂, которые имеют наибольший общий унификатор и , для некоторых дизъюнктов и . В этом случае резольвента определяется как

.

Здесь (D) – результат подстановки  в дизъюнкт D, определённый как (R(t₁, …, t_n)) = = R(t₁, …, t_n) для атомных формул, (R) = (R) для литералов, и (B₁  …  B_n)= =(B₁)  …  (B_n) для дизъюнктов.

Алгоритм доказательства выводимости ₁, ₂, …, _m , в предположении, что  и _i, 1  i  m, не имеют кванторов, будет следующим:

1. формулу ₁ & …& _m &  переводим в конъюнкцию дизъюнктов D₁&D₂&…&D_n, и переменные переименовываются таким образом, что D_i и D_j не содержат одинаковых переменных при i  j;

2. устанавливаем множество дизъюнктов: F = {D₁, D₂, …, D_n}.

3. если среди элементов из F нет резольвируемых, то выводимость не имеет места, заканчиваем работу;

4. если 0  F, то F противоречиво, а выводимость имеет место, заканчиваем работу;

5. берём резольвируемые дизъюнкты D_i и D_j из F, устанавливаем:

F = F  {Res (D_i, D_j)}

(этот шаг включает унификацию некоторых литералов), переходим к шагу 3.

Следующий пример принадлежит Робинсону.

Пример 2

Докажем выводимость P(a, b), Q(z) P(xy) & Q(y). После переноса правой части в левую часть получаем множество дизъюнктов:

F = {P(ab), Q(z), P(xy)  Q(y)}.

Наибольший общий унификатор для P(ab) и P(xy) равен: {a = x, b = y}.

Добавим к F резольвенту:

Res (P(ab), P(xy)  Q(y)) = Q(y).

Имеем: F = {P(ab), Q(z), P(xy)  Q(y), Q(y)}. Резольвента Res (Q(z), Q(y)) = 0 приводит к противоречивости F. Стало быть, выводимость имеет место. Легко видеть, что для данного примера существуют другие пути применения метода резолюций.

Существуют различные модификации метода резолюций.

В методе резолюций участвует также правило склейки, оно позволяет из дизъюнкта R(s₁, …, s_n)  R(t₁, …, t_n)  B₁  …  B_m получить (R(s₁, …, s_n)  B₁  …  B_m), (а из дизъюнкта R(s₁, …, s_n)  R(t₁, …, t_n)  B₁  …  B_m – дизъюнкт (R(s₁,…, s_n)  B₁  …  B_m)) , где  – наибольший общий унификатор системы уравнений s₁ = t₁, …, s_n = t_n.