Нормальные формы. 3.4.1. Предваренная нормальная форма

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

Определение. Формула А логики предикатов задана в предварен­ной (или в пренексной) нормальной форме, если она имеет вид (Q₁x₁)...Q_kx_k)В(х₁,...,х_k), где Q_i Î { $, " }, i = 1,2,...,k, а В есть бескванторная формула.

Теорема. Для всякой формулы А в ЛП существует равносильная ей формула в предваренной нормальной форме.

Доказательство. Индукция по построению формулы А. Пусть число логических связок в формуле А равно k.

БАЗИС. k = 0. Тогда А есть элементарная формула без кванторов; поэтому формула А находится в предваренной нормальной форме.

ПРЕДПОЛОЖЕНИЕ ИНДУКЦИИ. Допустим, что теорема верна для всякой формулы с числом логических связок меньше k.

ШАГ ИНДУКЦИИ. Покажем, что теорема справедлива для всякой формулы с числом логических связок k. Пусть формула А имеет k логических связок. Возможны следующие случаи.

1. А есть (Qx)B(x), где Q Î { $, " }. Так как глубина построения формулы В(х) меньше k, то по предположению индукции формула В(х) представима в предваренной нормальной форме С(х). Тогда (Qx)C(x) есть предваренная нормальная форма формулы А.

2. А есть В * С, где знак * Î {&, V, ® }. Так как число ло­гических связок в формулах В и С меньше k, то по предположению индукции существуют предваренные нормальные формы Е и F для фор­мул В и С соответственно. Пользуясь доказанными в п.3.3 равносильностями 1-18, выносим в формуле
Е * F кванторы за скобки и по­лучаем искомую предваренную нормальную форму для формулы А.

3. А есть ù В. Так как число логических связок в формуле В меньше k, то по предположению индукции формула В имеет предварен­ную нормальную форму (Q₁x₁)…(Q_kx_k)C, где С есть бескванторная формула. Тогда формула ù В имеет предваренную нормальную форму (Q’ ₁ x ₁ )...( Q'_k x _k ) ù C, где Q’_i есть $, если Q_i есть ", и Q’_i есть ", если Q_i есть $, i = 1,2,...,k.

Пример. (" y)(ù P(x) ® Q(y)) ® ($ y)(ù (" z)(P(y) V Q(z))) =
((" y)(ù P(x) ® Q(y))) V ($y)($ z) ù (P(y) V Q(z)) =
($ у) ù (ù Р(х) V Q(y)) V ($ y)($ z)(ù ù P(y) & ù Q(z)) =
($ y)(ù P(x) ® Q(y)) V ($ z)(P(y) & ù Q(z)) =
($ y)($ z)) ù P(x) ® Q(y))V P(y) & ù Q(z)).

3.4.2. Стандартная форма Скулема

Пусть А есть замкнутая формула логики предикатов. Приведем ее к пренексной (т.е. к предваренной) нормальной форме А₁ = (Q ₁x₁)…(Q _kx_k)
B₁(х₁,...,х_k). Пусть Q _r в формуле А, есть первый слева квантор существования, т.е. А₁ = (" x₁)...(" x_r-1)($ x_r) (Q _r+1x_r+1)...(Q _kx_k)B₁(x₁,...,x_r-1,x_r,x_r+1,...,x_k). Выберем новый, ранее не встречавшийся (r-1)-местный функциональный символ f, и перейдем к формуле А₂ = (" x₁)...(" x_r-1)(Q x_r+1)...(Q x_k)

Если r = 1, то в формуле A _lуберем квантор ($ х₁) и вместо х₁, находящегося в области действия квантора ($ х₁), подставим в А₁ константу а, ранее в А ₁не встречавшуюся.

Утверждение 1. Формула А ₁невыполнима тогда и только тогда, когда А₂ невыполнима.

Доказательство. Пусть формула А₁ невыполнима. Покажем, что
формула А₂ невыполнима. Допустим противное: А₂ выполнима, т.е.
существует множество D, предикаты и функции, определенные на D,
предметы из D такие, что высказывание ("x₁)...("x_r-1)(Q _r+1x_r+1)...(Q _kx_k)
B _l(x₁,... ,x_{r- 1} ,f (x₁,... ,x_r-1),x_г+1,... ,x_k) истинно. Тог­да для всяких x _l ,...,x_{r- 1}из D существует х_r = f (x ₁,... ,х_{r- 1} ) из D такое, что высказывание (Q _r+1x_r+1)… (Q _kx_k ) B_l (x _l, … ,x_{r- 1} ,x_r,x_{r+ l} ,…, x_k) истинно, т.е. высказывание (" x ₁,…
("x_r-1)($x_r) (Q _r+1 x_{r+ l} )... (Q_kx_k) B ₁ (x _l ,...,x_{r- 1} ,x_r,x_{r+ 1} ,...,x_k) истинно. Поэтому формула А₁ выполнима. Противоречие с невыполнимостью A₁. Следова­тельно, формула А₂ невыполнима.

Пусть формула А₂ невыполнима. Покажем, что формула А₁ невыпол­нима. Допустим противное: A₁ выполнима. Тогда существует множе­ство D, предикаты и функции, определенные на D, предметы из D, для которых высказывание (" x ₁,...("x_r-1)($x_r)(Q _r+1 x_{r+ l} )…(Q_kx_k)B ₁ (x _l ,...,x_{r- 1} ,x_r,x_{r+ 1} ,...,x_k) истинно. Тогда для всяких x₁,..., x_{r- 1}из D существует x_r из D, т.е. существует функция
x_r = f(x₁,..., x _r-1): D ^r-1 ® D, для которой высказывание

(Q _r+1 x_{r+ l} )...(Q_kx_k)B ₁ (x _l ,...,x_{r- 1} ,x_r,x_{r+ 1} ,...,x_k)

истинно. Тогда высказывание

(" x ₁)...("x_r-1)(Q _r+1 x_{r+ l} )B ₁ (x _l ,...,x_{r- 1}, f(x₁,…,x_{r- 1} ),x_{r+ 1} ,…,x_k)

истинно, т.е. формула А₂ выполнима. Противоречие с невыполнимос­тью А₂. Следовательно, формула А₂ невыполнима.

Утверждение 1 доказано.

Отметим теперь первое слева вхождение квантора существования в формуле А₂. Проделаем аналогичное устранение этого квантора. Получим формулу A₃. В ней проведем устранение первого слева кван­тора существования. И так далее, пока все кванторы существования не будут устранены (за счет введения новых функциональных сим­волов. В результате получим новую формулу D без кванторов сущест­вования, называемую стандартной формой Скулема. Функции, воз­никающие при построении этой стандартной формы, называются скулемовскими.

Утверждение 2. Формула А невыполнима тогда и только тогда, когда ее стандартная форма Скулема невыполнима.

Доказательство следует издоказанного выше утверждения 1, справедливого при каждом новом устранении из формулы А квантора существования.

Пример. А = ($x₁)("x₂)($x₃)("x₄)(P(x₁,x₂,x₃) ® Р(х₂,х₃,х₄)).

Вместо х₁ ставим константу а. Получаем формулу

("x₂) ($x₃)("x₄)(P(a,x₂,x₃) ® Р(х₂,х₃,х₄)).

Переменную х₃ заменяем на f(x₂), в результате получаем формулу

В = ("x₂)("x₄)(P(a,x₂,f(x₂)) ® P(x₂,f(x₂),x₄)).

Формула В есть стандартная форма Скулема формулы А.

Замечание. В стандартной форме Скулема бескванторную ее часть обычно представляют в конъюнктивной нормальной форме и рассмат­ривают как множество дизъюнктивных слагаемых (дизъюнктов). Кван­торы общности для этого множества дизъюнктов опускают.

3.5. Проблема разрешимости в логике предикатов

Основной вопрос математической логики есть проблема разреши­мости ее формул, т.е. вопрос об установлении общезначимости (или формальной доказуемости) формул этой логики. Проблема разрешимос­ти в ЛП состоит в существовании алгоритма, который по любой фор­муле логики предикатов устанавливал бы, является эта формула об­щезначимой или не является.

Теорема (А.Черча). Проблема распознавания общезначимости

формул логики предикатов алгоритмически неразрешима.

Б. А. Трахтенброт установил алгоритмическую неразрешимость ЛП на конечных классах: проблема разрешимости в ЛП остается неразре­шимой, если при установлении общезначимости формул ЛП ограничим­ся конечными множествами.

Хотя и не существует алгоритма, который по любой предъявлен­ной формуле в ЛП устанавливал бы, является эта формула общезна­чимой или не является, возможны попытки отыскания таких алгорит­мов для некоторых классов формул логики предикатов. Были найдены, например, алгоритмы, устанавливающие общезначимость класса замк­нутых формул, предваренные нормальные формы которых содержат только кванторы существования. Существует алгоритм распознавания общезначимости класса замкнутых формул, предваренные нормальные формы которых содержат только кванторы общности. Алгоритмически разрешим класс формул, построенных только из одноместных предика­тов (монадическая логика). Монадическая логика остается разреши­мой, даже если допустить кванторы по предикатным переменным. Ока­зался алгоритмически разрешимым ряд других классов формул логики предикатов. Исследования по установлению разрешающих алгоритмов в ЛП показали, что относительно мало классов формул имеют разрешаю­щие алгоритмы. Многие классы формул оказались алгоритмически не­разрешимыми. Работа по отысканию разрешающих алгоритмов продолжа­ется и поныне.

В семидесятые годы XX века был разработан универсальный язык программирования Пролог, в основу которого была положена ло­гика предикатов. Вычисление общезначимости формул в Прологе про­водится в приведенном Дж.А.Робинсоном логическом формализме, на­зываемом методом резолюций. В последующем мы изложим этот метод и покажем, как он используется в универсальном языке программирова­ния Пролог.