§7. Нормальные формы формул логики предикатов.
В логике предикатов, как и в логике высказываний, формулы могут иметь нормальную форму, т. е. существуют эквивалентные нормальные формы представления любых предикатных формул. При этом, используя равносильности алгебры высказываний и логики предикатов, каждую формулу логики предикатов можно привести к нормальной форме. В логике предикатов различают два вида нормальных форм: приведенную и предваренную.
Говорят, что формула логики предикатов имеет приведенную нормальную форму, если она содержит только операции конъюнкции, дизъюнкции и кванторные операции, а операция отрицания отнесена к элементарным формулам.
.
Получили приведенную нормальную форму исходной формулы.
Среди нормальных форм формул логики предикатов выделяют так называемую предваренную (префиксную, пренексную) нормальную форму (ПНФ). В ней кванторные операции либо полностью отсутствуют, либо они используются после всех операций алгебры логики, т. е. ПНФ формулы логике предикатов имеет вид
,
где под символом понимается один из кванторов или , а формула А кванторов не содержит.
Процедура получения (приведения) ПНФ. Состоит в следующем:
1. Используя формулы 18, 19 (отнесенные к предикатам), заменить операции и
на .
2. Используя форм, а также форм, 17, представить предикатную формулу таким образом, чтобы символы отрицания относились непосредственно к символам предикатов (и, таким образом, мы приводим исходную формулу к приведенной форме).
3. Для формул, содержащих подформулы вида , вести новые переменные, позволяющие использовать соотношения 46, 47, 49, 50 или 53, 54.
4. С помощью формул 35 – 38, 46, 47, 49, 50, 53, 54 получить формулу в виде ПНФ.
обозначим в предикате Q переменную y через z
обозначим в предикате Q переменную x через z
– ПНФ.
последний предикат не зависит от переменной z
два первых предиката не зависят от переменной u — ПНФ.
Определение. Формула логики предикатов, в которой из операций логики высказываний имеются только конъюнкция, дизъюнкция и отрицание, причем отрицание относится только к элементарным предикатам, называется Приведенной формой предиката.
Теорема 1. Для всякого предиката существует равносильная ему приведенная нормальная форма.
Доказательство. Действительно, все операции в данной предикатной формуле можно выразить через конъюнкцию, дизъюнкцию и отрицание (например, в виде ДНФ). Если после этого некоторые отрицания будут относиться к частям формулы, содержащим кванторы, то отрицания можно “снять” с кванторов согласно равносильностям 1 и 2, а “снять” отрицания с конъюнкций и дизъюнкций можно, следуя законам де Моргана. После всех описанных преобразований предикат, очевидно, будет представлен в приведенной форме.
Определение. Предикатная формула вида , где КI – кванторы, ХI – различные связанные переменные, а F – Предикатная формула без кванторов, находящаяся в приведенной форме, называется Предваренной нормальной формой предиката.
Теорема 2. Для всякого предиката существует равносильная ему предваренная нормальная форма.
Доказательство. Согласно теореме 1 можно считать, что предикат уже преобразован в приведенную форму. Если никакая операция навешивания квантора при этом не находится в области действия операций и , то приведенная форма уже является предваренной нормальной. Поэтому предположим, что описанные ситуации имеют место, и будем называть такие явления (когда какой–либо квантор находится в области действия данной операции или ) Беспорядками.
Для данной формулы число беспорядков конечно, так как конечно число символов. Выберем какой-либо беспорядок (скажем, первый слева) и покажем, что путем тождественных преобразований его можно убрать. Возможны два случая:
1) Беспорядок имеет вид: "X Р или $Х Р, где Р – не зависит от Х. Тогда "Х или $Х можно просто отбросить, поскольку "ХР º Р и $ХР º Р.
2) Беспорядок имеет вид: "ХР(Х) или $ХР(Х). Если переменная Х еще встречается в формуле, то предварительно сделав замену согласно формулам
Где T – переменная, не встречающаяся в формуле, беспорядок представляется в виде правой части одной из формул 10 – 13. Применяя эти формулы (т. е., заменяя правые части на левые), беспорядок устраняется.
Проделав такие преобразования конечное число раз, все беспорядки будут ликвидированы, что и требовалось доказать.
Пример. Привести к предваренной нормальной форме следующий предикат:
Для того, чтобы оценить ресурс, необходимо авторизоваться.
Учебное пособие предназначено для студентов МАТИ, изучающих дисциплины "Математическая логика и теория алгоритмов" и "Дискретная математика", обучающихся по специальностям "Информатика и вычислительная техника" и "Системы автоматизированного проектирования". Оно ставит своей целью помочь студентам лучше усвоить теоретический и практический материал. Пособие посвящено изучению важных разделов математической логики (алгебры высказываний, логики предикатов) и теории алгоритмов. Его основу составляют конспекты лекций, которые читались студентам. Данное пособие содержит большое количество примеров, иллюстрирующих основные понятия указанных разделов математической логики и теории алгоритмов и утверждения, касающиеся этих понятий. Издание также может быть полезно для студентов других специальностей и преподавателей.