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

ПРОБЛЕМА РАЗРЕШИМОСТИ.

ТЕОРИЯ АВТОМАТИЧЕСКОГО ВЫВОДА

Логика предикатов является основанием конкретных прикладных теорий. Поэтому основной проблемой в ней является выяснение общезначимости её формул (будут ли они её теоремами). Если формула А исчисления предикатов общезначима, то она может быть использована для логи-ческих рассуждений в любой теории первого порядка К. Если не общезначима, то при её применении могут быть получены (не обязательно) ошибочные суждения.

Выяснение общезначимости формул в любой матема-тической логике называется проблемой разрешимости. В неформальных логиках для проверки общезначимости мо-гут использоваться любые математические приёмы. Напри-мер, в алгебре логики – построение таблиц истинности для функций, реализующих формулы. В нечеткой логике – вы-числение значения истинности на области определения соответствующих функций. В формальных логических теориях (ИВ, ИП) для проверки общезначимости формулы А можно использовать только формальные приёмы – постро-ить вывод А из аксиом теории, доказать опровержимость формулы Ø А и т. д. Таким образом, проверка обще-значимости формул в ИП может быть сведена к проблеме существования алгоритма разрешимости, позволяющего для каждой формулы выяснить её общезначимость. В общем случае ответ на этот вопрос даёт

Теорема Чёрча. Проблема разрешимости в ИП алго-ритмически не разрешима.

Хотя теорема утверждает, что общего алгоритма (при-менимого ко всем формулам ИП) проверки разрешимости не существует, такие алгоритмы построены для отдельных классов формул, в частности, для формул монадической ло-

гики, в которой допускаются только одноместные кванторы.

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

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

Основными способами проверки общезначимости формул являются:

1) построение их вывода из аксиом теории и

2) доказательство невыполнимости их отрицания (любая интерпретация опровергает его).

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

Определение. Пренексной нормальной формой (ПНФ) называется представление в ЛП формулы А следую-щего вида:

А¢ =(Q₁ (x₁) Q₂ (x₂)...Q_n (x_n))М,

где =(Q₁ (x₁) Q₂ (x₂)...Q_n (x_n)) - начальная часть формулы, содержащая кванторы, называется префиксом (приставкой), а бескванторная часть формулы М - матрицей.

Определение. Для упрощения дальнейшего анализа матрицу М представляют в форме конъюнкциидизъюнктов: М = (D₁ & D₂ &...& D_k),

где все дизъюнкты D_i (1 £ i £ k) являются логическими сум-мами конечного числа литер либо их отрицаний. Под лите-рами понимаются атомы - предикаты, зависящие только от термов.

Примеры литер. 1) Q(x), 2) P(x,b), 2) R(f(x), g(x,а)).

Примеры дизъюнктов. 1) P(x,y)ÚØR(b,x,z), 2) Ø Q(x) Ú P(f(x, a), b), 3) R(x,a,b).

Поскольку в разрешающих алгоритмах используются пренексные нормальные формы с представлением матриц в виде конъюнкции дизъюнктов, рассмотрим алгоритм пере-хода от формулы ЛП произвольного вида А к пренексной форме с матрицей данного вида. Алгоритм можно разбить на несколько последовательных шагов. Рассмотрим их, иллюстрируя применение на примере преобразования фор-мулы А= "х Р(х) ® $ y(Q(x,у) º Р(х)).

1. Исключить из А все логические связки “º“ (эквива-лентность).

Для этого используем тавтологию (ВºС)º (В ® С)&(С ®В). В примере после замены

(Q(x,у) º Р(х)) º (Q(x,у) ® Р(х))&(Р(х))® Q(x,у))

получим:

А= "х Р(х) ® $ y((Q(x,у) ® Р(х))&(Р(х))® Q(x,у))).

2. Исключить из А все логические связки “ ® “ (импли-кация).

Для этого используем правило замены (В®С) º (Ø ВÚ С). Во всех заменах необходимо учитывать очередность вы-полнения операций, предписанную структурой формулы. В примере вначале выполняем замены в области действия квантора $ y:

(Q(x,у) ® Р(х)) º (ØQ(x,у) Ú Р(х)),

(Р(х)® Q(x,у)) º (ØР(х) Ú Q(x,у)).

При этом получаем формулу вида:

А= "х Р(х) ® $ y((ØQ(x,у) Ú Р(х)) & (ØР(х) Ú Q(x,у))).

Заменяя оставшуюся импликацию, в итоге получим:

А= Ø ("хР(х)) Ú $ y((ØQ(x,у) Ú Р(х)) & (ØР(х) Ú Q(x,у))).

После применения пунктов 1 и 2 в формуле остаются только логические связки Ø, Ú и &.

3. Внести отрицание ( Ø) вглубь формулы.

После выполнения операции отрицание не должно стоять перед скобками либо перед кванторами, а может быть только перед предикатами. Для этого используются законы де Моргана и следующие равносильности формул ИП:

1) Ø" х B(х) º $ xØ B(x),

2) Ø $х B(х) º " xØ B(x).

В примере, используя закон 1), получим:

А = $х(Ø Р(х)) Ú $ y((ØQ(x,у) Ú Р(х)) & (ØР(х) Ú Q(x,у))).

4. Вынести кванторы в начало формулы.