Математическая логика и теория алгоритмов. Стенюшкина В.А. - 36 стр.

      F0 – формула, не имеющая кванторов.
      Цепочка Q1 x1 … Qn xn называется предикатом, F0 – матрицей.
      Пример - Формула ∀x∀y∃z (Q(x,y) →R(z)) находится в ПНФ.
      Для любой формулы ЛП существует логически эквивалентная ей форму-
ла, находящаяся в ПНФ.
      Приведение данной формулы ЛП к ПНФ можно произвести с помощью
равносильностей (1-6) и следований (7-8).
      Пример - Привести формулу ∀x Р(x) →∃ x Q(x) к ПНФ.
      Решение - ∀x Р(x) →∃ x Q(x)= ((∀x Р(x))∨ ∃ x Q(x)= ∃ x ((∀x Р(x)) ∨ ∃ x
Q(x)= ∃ x((Р(x)) ∨ Q(x)).
      Следовательно, ПНФ для исходной формулы есть ∃ x(( Р(x)) ∨ Q(x)).

      12.5 Скулемовская стандартная форма

       Доказательство теорем сопутствует основной задаче логики предикатов –
описание всех тождественно – истинных формул. Согласно методу резолюций
вместо доказательства тавтологичности формулы доказывается, что отрицание
формулы противоречиво. Для этого формула приводится к скулемовской стан-
дартной форме, или стандартной форме. Ранее обсуждалось, как свести форму-
лу ЛП к ПНФ. Дальнейшее преобразование касается матрицы и префикса. Тех-
ника сведения бескванторной формулы (здесь - матрицы) к конъюнктивной
нормальной форме также показана ранее. Теперь займемся элиминацией (уст-
ранением) кванторов.
       Пусть формула F находится в предваренной нормальной форме Q1 x1 …
Qn xn F0, где F0 есть конъюнктивная нормальная форма. Если Qr, 1≤ r ≤n, есть
квантор единичности в префиксе Q1x1…Qn xn, рассмотрим случаи:
       1) никакой квантор общности не стоит в префиксе левее Qr. Тогда выби-
раем новую ( не встречавшуюся в формуле) константу с и заменяем все xr в F0
на с; вычеркиваем Qr xr из префикса;
       2) имеется непустой список Qr1, …, Qrm, 1≤ r1≤ …≤rm< r, всех кванторов
общности, встречающихся в префиксе левее Qr. Тогда выбираем новый ( не
встречавшийся в формуле функциональный символ f, заменяем все xr в F0 на
f(xr1, …, xrm).
       Выполняем эту процедуру для всех кванторов существования в префиксе.
Полученная в результате формула имеет, по определению, скулемовскую стан-
дартную форму. Константы и функторы, используемые для замены переменных
кванторов существования, называются скулемовскими функциями.
       Пример – Указать ССФ формулы ∃ x ∀y ∀ z ∃u∀v ∃w P(x,y,z,u,v, w).
       Ответ - ∀y ∀ z∀v P(x, y, z, f(y, z), v,g(y, z, v)).
       Введем термины: литерал (атом или отрицание атома), дизъюнкт (дизъю-
нкция литералов). Дизъюнкт, не содержащий литералов, назовем пустым дизъ-
юнктом. Множеством дизъюнктов назовем конъюнкцию всех дизъюнктов из S ,
где каждая переменная в S управляется квантором общности. По этому согла-
шению стандартная форма может быть представлена множеством дизъюнктов.