Основные понятия и методы теории формальных систем. Волохович А.В. - 7 стр.

   данный факт далее будет играть принципиальное значение.
  Литерами будем называть атомы и их отрицания. Таким образом,
формула ( ¬ А ∨ В) составлена из двух литер, ¬ А и B.
  Формула В есть конъюнктивная нормальная форма (КНФ), если В
имеет вид

                  В 1 &В 2 & ...& В m ,

где каждая из формул B i , i=1,…,m, есть дизъюнкция литер. В
качестве примера КНФ приведем формулу:

           ( ¬ X 1 ∨ X 3 ∨ ¬ X 4 )& (X 1 ∨ X 2 )& (X 2 ∨ ¬ X 3 ∨ X 5 ).

  Аналогично, формула В есть дизъюнктивная нормальная форма
(ДНФ), если В имеет вид

                  В 1 ∨ В 2 ∨ ... ∨ В m ,

где каждая из формул B i , i=1,…,m, есть конъюнкция литер. В
качестве примера ДНФ приведем формулу:

           ( ¬ X 1 & X 3 & ¬ X 4 ) ∨ (X 1 & X 2 ) ∨ (X 2 & ¬ X 3 & X 5 ).

   В дальнейшем дизъюнкцию литер будем называть дизъюнктом, а
конъюнкцию – конъюнктом.
   Любая формула ИВ может быть преобразована в эквивалентную
ей ДНФ или КНФ с помощью следующего алгоритма.

    Шаг 1. А → В = ¬ А ∨ В,
           А~В = (А ∨ ¬ В)& ( ¬ А ∨ В)
    выражение операций импликации и эквиваленции через операции
    конъюнкции и дизъюнкции.

    Шаг 2. ¬ ¬ А=A ,
           ¬ (А ∨ В) = ¬ А& ¬ В,
           ¬ (А&В) = ¬ А ∨ ¬ В
     продвижение отрицания до атома.

    Шаг 3. А ∨ (В&C) = (А ∨ В)& (А ∨ C) (для КНФ),
           А& (В ∨ C) = (А&В) ∨ (А&C) (для ДНФ).

Пример 1. Требуется преобразовать в КНФ формулу

           Ф=[( ¬ А → В)& ¬ (C&(D → А))].



7