В булевой логике , A формула находится в конъюнктивной нормальной форме ( КНФ ) или клаузальной нормальной форме , если это соединение одного или несколько положений , где раздел представляет собой дизъюнкцию из литералов ; иначе говоря, это произведение сумм или И или ИЛИ . Как каноническая нормальная форма , она полезна в автоматическом доказательстве теорем и теории цепей .
Все союзы литералов и все дизъюнкции литералов находятся в CNF, поскольку их можно рассматривать как союзы однобуквенных предложений и союзов одного предложения, соответственно. Как и в дизъюнктивной нормальной форме (ДНФ), единственные пропозициональные связки, которые может содержать формула в КНФ, - это и , или , и not . Оператор not может использоваться только как часть литерала, что означает, что он может предшествовать только пропозициональной переменной или символу предиката .
В автоматическом доказательстве теорем понятие « нормальная форма клаузии » часто используется в более узком смысле, имея в виду конкретное представление формулы CNF в виде набора наборов литералов.
Примеры и не примеры
Все следующие формулы в переменных , а также находятся в соединительной нормальной форме:
Для ясности дизъюнктивные предложения написаны выше в круглых скобках. В дизъюнктивной нормальной форме с заключенными в скобки конъюнктивными предложениями последний случай такой же, но предпоследний -. Константы true и false обозначаются пустым конъюнктом и одним предложением, состоящим из пустого дизъюнкта, но обычно записываются явно. [1]
Следующие формулы не имеют конъюнктивной нормальной формы:
- , поскольку ИЛИ вложено в НЕ
- , так как И вложено в ИЛИ
Любую формулу можно эквивалентно записать в виде формулы в конъюнктивной нормальной форме. Три не примеров в CNF:
Преобразование в CNF
[2] Каждая пропозициональная формула может быть преобразована в эквивалентную формулу в CNF. Это преобразование основано на правилах логической эквивалентности : исключении двойного отрицания , законах Де Моргана и распределительном законе .
Поскольку все пропозициональные формулы могут быть преобразованы в эквивалентные формулы в конъюнктивной нормальной форме, доказательства часто основываются на предположении, что все формулы являются КНФ. Однако в некоторых случаях это преобразование в CNF может привести к экспоненциальному взрыву формулы. Например, перевод следующей формулы, не относящейся к CNF, в CNF дает формулу с статьи:
В частности, полученная формула:
Эта формула содержит статьи; каждое предложение содержит либо или же для каждого .
Существуют преобразования в CNF, которые избегают экспоненциального увеличения размера, сохраняя выполнимость, а не эквивалентность . [3] [4] Эти преобразования гарантируют только линейное увеличение размера формулы, но вводят новые переменные. Например, приведенная выше формула может быть преобразована в CNF путем добавления переменных следующим образом:
Интерпретация удовлетворяет эта формула только тогда , когда по крайней мере один из новых переменных верно. Если эта переменная, то оба а также также верны. Это означает, что каждая модель , удовлетворяющая этой формуле, также удовлетворяет исходной. С другой стороны, только некоторые из моделей исходной формулы удовлетворяют этой: посколькуне упоминаются в исходной формуле, их значения не имеют отношения к ее удовлетворению, чего нет в последней формуле. Это означает, что исходная формула и результат перевода равнозначны, но не эквивалентны .
Альтернативный перевод, преобразование Цейтина , включает также предложения. С этими пунктами формула подразумевает; эта формула часто считается "определяющей" быть именем для .
Логика первого порядка
В логике первого порядка конъюнктивная нормальная форма может быть взята дальше, чтобы получить клаузальную нормальную форму логической формулы, которую затем можно использовать для выполнения разрешения первого порядка . В автоматическом доказательстве теорем на основе разрешающей способности формула CNF
, с участием литералы, обычно представляется как набор наборов | |||||||||||||||||||
. |
См ниже в качестве примера.
Вычислительная сложность
Важный набор проблем вычислительной сложности включает нахождение присвоений переменным булевой формулы, выраженной в конъюнктивной нормальной форме, таким образом, чтобы формула была истинной. Задача k -SAT - это проблема нахождения удовлетворительного присваивания булевой формуле, выраженной в CNF, в которой каждая дизъюнкция содержит не более k переменных. 3-SAT является NP-полной (как и любая другая задача k -SAT с k > 2), в то время как 2-SAT, как известно, имеет решения за полиномиальное время . Как следствие, [5] задача преобразования формулы в ДНФ с сохранением выполнимости является NP-трудной ; в общем , преобразование в CNF с сохранением достоверности также является NP-трудным; следовательно, преобразование с сохранением эквивалентности в DNF или CNF снова является NP-трудным.
Типичные проблемы в этом случае связаны с формулами в "3CNF": конъюнктивная нормальная форма с не более чем тремя переменными на конъюнкт. Примеры таких формул, встречающихся на практике, могут быть очень большими, например, со 100 000 переменных и 1 000 000 конъюнктов.
Формула в CNF может быть преобразована в равно удовлетворяемую формулу в « k CNF» (для k ≥3) путем замены каждого конъюнкта более чем на k переменных. двумя конъюнктами а также с новой переменной Z и повторением по мере необходимости.
Преобразование из логики первого порядка
Чтобы преобразовать логику первого порядка в CNF: [2]
- Преобразовать в нормальную форму отрицания .
- Устранение последствий и эквивалентностей: неоднократно заменять с участием ; заменять с участием . В конце концов, это устранит все вхождения а также .
- Переместите НЕ внутрь, многократно применяя закон Де Моргана . В частности, замените с участием ; заменять с участием ; и заменить с участием ; заменять с участием ; с участием . После этого может встречаться только непосредственно перед предикатным символом.
- Стандартизируйте переменные
- Для предложений вроде которые используют одно и то же имя переменной дважды, измените имя одной из переменных. Это позволяет избежать путаницы при отбрасывании кванторов. Например, переименован в .
- Сколемизируйте заявление
- Переместить кванторы наружу: повторно заменить с участием ; заменять с участием ; заменять с участием ; заменять с участием . Эти замены сохраняют эквивалентность, поскольку предыдущий шаг стандартизации переменных гарантировал, что не встречается в . После этих замен квантификатор может встречаться только в начальном префиксе формулы, но никогда внутри, , или же .
- Неоднократно заменять с участием , где это новый -арный функциональный символ, так называемая « сколемская функция ». Это единственный шаг, который сохраняет только выполнимость, а не эквивалентность. Он устраняет все экзистенциальные кванторы.
- Отбросьте все универсальные кванторы.
- Распределите ИЛИ внутрь по И: повторно замените с участием .
Например, формула «Любой, кто любит всех животных, в свою очередь, кого-то любит» преобразуется в CNF (а затем в форму предложения в последней строке) следующим образом (выделение редексов правила замены в):
на 1,1 | ||||||||||||||||||||||||||||||||||||
на 1,1 | ||||||||||||||||||||||||||||||||||||
на 1,2 | ||||||||||||||||||||||||||||||||||||
на 1,2 | ||||||||||||||||||||||||||||||||||||
на 1,2 | ||||||||||||||||||||||||||||||||||||
на 2 | ||||||||||||||||||||||||||||||||||||
на 3,1 | ||||||||||||||||||||||||||||||||||||
на 3,1 | ||||||||||||||||||||||||||||||||||||
на 3,2 | ||||||||||||||||||||||||||||||||||||
по 4 | ||||||||||||||||||||||||||||||||||||
на 5 | ||||||||||||||||||||||||||||||||||||
( представление статьи ) |
Неформально функция Сколема можно рассматривать как уступку человеку, который любим, в то время как дает животное (если есть), которое не любит. Третья последняя строка снизу читается как " не любит животное , или иначе любит " .
2-я последняя строка сверху, , является CNF.
Заметки
- ^ Питер Б. Эндрюс, Введение в математическую логику и теорию типов , 2013, ISBN 9401599343 , стр. 48
- ^ a b Искусственный интеллект: современный подход. Архивировано 31 августа 2017 г. в Wayback Machine [1995 ...] Рассел и Норвиг.
- ^ Цейтин (1968)
- ^ Джексон и Шеридан (2004)
- ^ так как один из способов проверить CNF на выполнимость - это преобразовать его в DNF , выполнимость которого может быть проверена за линейное время.
Смотрите также
- Алгебраическая нормальная форма
- Дизъюнктивная нормальная форма
- Оговорка о роге
- Алгоритм Куайна – Маккласки
Рекомендации
- Дж. Элдон Уайтситт (24 мая 2012 г.). Булева алгебра и ее приложения . Курьерская корпорация. ISBN 978-0-486-15816-7.
- Ханс Кляйне Бюнинг; Теодор Леттманн (28 августа 1999 г.). Логика высказываний: дедукция и алгоритмы . Издательство Кембриджского университета. ISBN 978-0-521-63017-7.
- Пол Джексон, Дэниел Шеридан: Преобразования форм предложения для логических схем . В: Holger H. Hoos, David G. Mitchell (Eds.): Theory and Applications of Satisfiability Testing, 7-я Международная конференция, SAT 2004, Ванкувер, Британская Колумбия, Канада, 10–13 мая 2004 г., Пересмотренные избранные статьи. Конспект лекций по информатике 3542, Springer 2005, стр. 183–198
- Г. С. Цейтин: О сложности вывода в исчислении высказываний . В кн .: Слисенко А.О. (ред.) Структуры в конструктивной математике и математической логике, часть II, Семинары по математике, с. 115–125. Математический институт им. В. А. Стеклова (1968)
Внешние ссылки
- "Конъюнктивная нормальная форма" , Энциклопедия математики , EMS Press , 2001 [1994]
- Java-апплет для преобразования в CNF и DNF, показывающий используемые законы