Заперечення нормальної форми

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до навігації Перейти до пошуку

В математичній логіці, формула є запереченням нормальної форми, якщо заперечення утворене оператором (, не), який може бути записаний або сам, або з логічними операторами: кон'юнкції (, і) і диз'юнкція (, або).

Заперечення нормальної форми не є канонічною формою: наприклад, і є еквівалентними, і обидва знаходяться в запереченні нормальній формі.

У класичній логіці і багатьох видах модальної логіки, кожна формула може бути приведена в цю форму, замінивши наслідки і еквівалентності їх визначеннями, використовуючи закони де Моргана, щоб підштовхнути запереченням до середини, і усунення подвійних заперечень. Цей процес можна представити за допомогою наступних правил переписування (Handbook of Automated Reasoning 1, с 204.):

Формула заперечення нормальної форми може бути використана в більш сильному КНФ або ДНФ шляхом застосування дистрибутивності.

Приклади і контрприклади[ред. | ред. код]

Наступні формули усі в запереченні:

Перший приклад в кон'юнктивній нормальній формі, а останні два в обох КНФ і ДНФ, але другий приклад ні в одному. Наступні формули не в запереченні:

Вони відповідно еквівалентні такими формулами з запереченням як:

Посилання[ред. | ред. код]

  • Alan J.A. Robinson and Andrei Voronkov, Handbook of Automated Reasoning 1:203ff (2001) ISBN 0444829490.

Посилання[ред. | ред. код]