Дизъюнкты и нормальные формы

Бывает полезно преобразовать заданную формулу в эквивалентную ей, имеющую вид «нормальной» или «канонической» формы.

Дизъюнктом называется дизъюнкция конечного числа высказываний, то есть формула вида или .

Конъюнктивной нормальной формой (КНФ) называется конъюнкция конечного числа дизъюнктов.

Теорема. Любая формула имеет логически эквивалентную ей КНФ.

Алгоритм нормализации:

1. Исключение связок эквивалентности и импликации.

2. Необходимое число раз применяются правила преобразования из законов де Моргана, чтобы отрицания перевести на уровень элементарных высказываний.

3. Необходимое число раз применяются законы дистрибутивности (раскрыть все скобки).

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

Нормальная форма общезначима тогда и только тогда когда все ее дизъюнкты общезначимы.

Дизъюнкт общезначим тогда и только тогда, когда он содержит пару противоположных высказываний.

Понятие дизъюнкта важно для практики. Описание задач и алгоритмов в терминах дизъюнктов составляет основу логического программирования.

Двойственным понятием к дизъюнкту является конъюнкт. Дизъюнктивная нормальная форма (ДНФ) – дизъюнкция конечного числа конъюнктов. Можно показать, что любая формула приводима к логически эквивалентной ей ДНФ.