Приведенные и нормальные формы в логике предикатов
Рассмотрим способ упрощения формул, опирающийся на приведенные равносильности.
Формулы, в которых из логических символов имеются только символы конъюнкция, дизъюнкция и отрицание, причем символ отрицания встречается над символами предикатов, будем называть приведенными.
Для любой формулы существует равносильная ей приведенная формула, причем множества свободных и связанных переменных этих формул совпадают.
Такая приведенная формула называется приведенной формой данной формулы.
В логике высказываний мы ввели две нормальные формы — дизъюнктивную нормальную форму и конъюнктивную нормальную форму.
В логике предикатов также имеется нормальная форма, цель которой — упрощение процедуры доказательств.
Приведенная формула называется нормальной, если она не содержит символов кванторов или все символы кванторов стоят впереди (т.е. логические символы и символы предикатов стоят в области действия каждого квантора).
