Множество ТИ-формул логики предикатов входит в любую теорию, исследование этого множества - важная цель логики предикатов. При этом выделяются две проблемы:
1) получение ТИ-формул (проблема построения порождающей процедуры для множества ТИ-формул);
2) проверка формулы на истинность (проблема разрешающей процедуры).
В отличие от логики (алгебры) высказываний в логике предикатов прямой перебор всех значений переменных может быть невозможен, если предметные переменные имеют бесконечные области определения. Поэтому в логике предикатов используются различные косвенные приемы, в том числе эквивалентные соотношения, позволяющие выполнить корректные преобразования предикатных формул. В логике (алгебре) предикатов справедливы все эквивалентные соотношения логики (алгебры) высказываний, а также собственные эквивалентные соотношения, включающие связки и (ниже под Y будем понимать переменное высказывание или формулу, не содержащую х):
Используя соотношения (2, 3) можно выразить один квантор через другой. Соотношения (4, 5) показывают дистрибутивность квантора общности относительно конъюнкции & и квантора существования относительно дизъюнкции v. Если в этих выражениях поменять местами кванторы и , то получим соотношения, верные лишь в одну сторону:
|
|
В таких случаях эквивалентных преобразований применяют переименование переменной х в одном из предикатов на новую переменную:
Соотношения (6, 7) отражают в некотором смысле коммутативность одноименных кванторов (возможность менять местами одноименные кванторы), что несправедливо для разноименных кванторов, например Р(х, у) и Р(х, у) не эквивалентны. Соотношения (8) - (11) позволяют формулу, не содержащую переменную х, выносить за пределы действия квантора, связывающего эту переменную.
Префиксной нормальной формой (ПНФ) называется формула, имеющая вид:
Q1x1Q2x2...QnxnF,
где Q1x1Q2x2...Qnxn - кванторы; F-формула, не имеющая кванторов, с операциями {&, v, -}.
Получение ПНФ:
1. Используя формулы
заменить операции {→, ~} на { &, v, -}.
2. Воспользовавшись выражениями (2), (3), а также правилом двойного отрицания и правилами де Моргана
представить предикатную формулу таким образом, чтобы символы отрицания были расположены непосредственно перед символами предикатов.
3. Для формул, содержащих подформулы вида
ввести новые переменные, позволяющие использовать соотношения (8) - (11).
4. С помощью формул (4) - (11) получить формулы в виде ПНФ.