Конъюнктивная нормальная форма - Conjunctive normal form

В булевой логике , A формула находится в конъюнктивной нормальной форме ( КНФ ) или клаузальной нормальной форме , если это соединение одного или несколько положений , где раздел представляет собой дизъюнкцию из литералов ; иначе говоря, это произведение сумм или И или ИЛИ . Как каноническая нормальная форма , она полезна в автоматическом доказательстве теорем и теории цепей .

Все союзы литералов и все дизъюнкции литералов находятся в CNF, поскольку их можно рассматривать как союзы однобуквенных предложений и союзов одного предложения, соответственно. Как и в дизъюнктивной нормальной форме (ДНФ), единственные пропозициональные связки, которые может содержать формула в КНФ, - это и , или , и not . Оператор not может использоваться только как часть литерала, что означает, что он может предшествовать только пропозициональной переменной или символу предиката .

В автоматическом доказательстве теорем понятие « нормальная форма клаузии » часто используется в более узком смысле, имея в виду конкретное представление формулы CNF в виде набора наборов литералов.

Примеры и не примеры

Все следующие формулы в переменных и имеют конъюнктивную нормальную форму: ${\ displaystyle A, B, C, D, E}$${\ displaystyle F}$

• ${\ Displaystyle (А \ лор \ нег В \ лор \ нег С) \ земля (\ нег Д \ лор Е \ лор F)}$
• ${\ Displaystyle (А \ лор В) \ земля (С)}$
• ${\ Displaystyle (А \ лор В)}$
• ${\ Displaystyle (А)}$

Для ясности дизъюнктивные предложения написаны выше в круглых скобках. В дизъюнктивной нормальной форме с заключенными в скобки конъюнктивными предложениями последний случай такой же, но предпоследний . Константы true и false обозначаются пустым конъюнктом и одним предложением, состоящим из пустого дизъюнкта, но обычно записываются явно. ${\ Displaystyle (А) \ лор (В)}$

Следующие формулы не имеют конъюнктивной нормальной формы:

• ${\ Displaystyle \ neg (В \ лор С)}$, поскольку ИЛИ вложено в НЕ
• ${\ Displaystyle (А \ земля В) \ лор С}$
• ${\ Displaystyle А \ земля (В \ лор (D \ земля E))}$, так как И вложено в ИЛИ

Каждую формулу можно эквивалентно записать как формулу в конъюнктивной нормальной форме. Три не примеров в CNF:

• ${\ Displaystyle (\ neg B) \ земля (\ neg C)}$
• ${\ Displaystyle (А \ лор С) \ земля (В \ лор С)}$
• ${\ Displaystyle (A) \ земля (B \ lor D) \ land (B \ lor E).}$

Преобразование в CNF

Каждую пропозициональную формулу можно преобразовать в эквивалентную формулу в CNF. Это преобразование основано на правилах логической эквивалентности : исключении двойного отрицания , законах Де Моргана и распределительном законе .

Поскольку все пропозициональные формулы могут быть преобразованы в эквивалентные формулы в конъюнктивной нормальной форме, доказательства часто основываются на предположении, что все формулы являются КНФ. Однако в некоторых случаях это преобразование в CNF может привести к экспоненциальному взрыву формулы. Например, перевод следующей формулы, отличной от CNF, в CNF дает формулу с пунктами: ${\ displaystyle 2 ^ {n}}$

${\ displaystyle (X_ {1} \ wedge Y_ {1}) \ vee (X_ {2} \ wedge Y_ {2}) \ vee \ dots \ vee (X_ {n} \ wedge Y_ {n}).}$

В частности, полученная формула:

${\ displaystyle (X_ {1} \ vee X_ {2} \ vee \ cdots \ vee X_ {n}) \ клин (Y_ {1} \ vee X_ {2} \ vee \ cdots \ vee X_ {n}) \ клин (X_ {1} \ vee Y_ {2} \ vee \ cdots \ vee X_ {n}) \ клин (Y_ {1} \ vee Y_ {2} \ vee \ cdots \ vee X_ {n}) \ клин \ cdots \ wedge (Y_ {1} \ vee Y_ {2} \ vee \ cdots \ vee Y_ {n}).}$

Эта формула содержит пункты; каждое предложение содержит одно или для каждого . ${\ displaystyle 2 ^ {n}}$${\ displaystyle X_ {i}}$${\ displaystyle Y_ {i}}$${\ displaystyle i}$

Существуют преобразования в CNF, которые избегают экспоненциального увеличения размера, сохраняя выполнимость, а не эквивалентность . Эти преобразования гарантируют только линейное увеличение размера формулы, но вводят новые переменные. Например, приведенная выше формула может быть преобразована в CNF путем добавления следующих переменных : ${\ Displaystyle Z_ {1}, \ ldots, Z_ {n}}$

${\ Displaystyle (Z_ {1} \ vee \ cdots \ vee Z_ {n}) \ клин (\ neg Z_ {1} \ vee X_ {1}) \ клин (\ neg Z_ {1} \ vee Y_ {1} ) \ wedge \ cdots \ wedge (\ neg Z_ {n} \ vee X_ {n}) \ wedge (\ neg Z_ {n} \ vee Y_ {n}).}$

Интерпретация удовлетворяет эта формула только тогда , когда по крайней мере один из новых переменных верно. Если эта переменная есть , то оба и также верны. Это означает, что каждая модель , удовлетворяющая этой формуле, также удовлетворяет исходной. С другой стороны, только некоторые из моделей исходной формулы удовлетворяют этой модели: поскольку они не упоминаются в исходной формуле, их значения не имеют отношения к ее удовлетворению, чего нет в последней формуле. Это означает, что исходная формула и результат перевода равнозначны, но не эквивалентны . ${\ displaystyle Z_ {i}}$${\ displaystyle X_ {i}}$${\ displaystyle Y_ {i}}$${\ displaystyle Z_ {i}}$

Альтернативный перевод, преобразование Цейтина , также включает в себя клаузулы . С этими пунктами формула подразумевает ; эта формула часто рассматривается как «определение» как название для . ${\ Displaystyle Z_ {я} \ vee \ neg X_ {i} \ vee \ neg Y_ {i}}$${\ Displaystyle Z_ {я} \ эквив X_ {я} \ клин Y_ {я}}$${\ displaystyle Z_ {i}}$${\ Displaystyle X_ {i} \ клин Y_ {i}}$

Логика первого порядка

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

${\ displaystyle (}$

${\ displaystyle l_ {11}}$

${\ Displaystyle \ lor}$

${\ displaystyle \ ldots}$

${\ Displaystyle \ lor}$

${\ displaystyle l_ {1n_ {1}}}$

${\ displaystyle)}$

${\ displaystyle \ land}$

${\ displaystyle \ ldots}$

${\ displaystyle \ land}$

${\ displaystyle (}$

${\ displaystyle l_ {m1}}$

${\ Displaystyle \ lor}$

${\ displaystyle \ ldots}$

${\ Displaystyle \ lor}$

${\ displaystyle l_ {mn_ {m}}}$

${\ displaystyle)}$

, с литералами, обычно представляется как набор наборов ${\ displaystyle l_ {ij}}$

${\ displaystyle \ {}$

${\ displaystyle \ {}$

${\ displaystyle l_ {11}}$

${\ displaystyle,}$

${\ displaystyle \ ldots}$

${\ displaystyle,}$

${\ displaystyle l_ {1n_ {1}}}$

${\ displaystyle \}}$

${\ displaystyle,}$

${\ displaystyle \ ldots}$

${\ displaystyle,}$

${\ displaystyle \ {}$

${\ displaystyle l_ {m1}}$

${\ displaystyle,}$

${\ displaystyle \ ldots}$

${\ displaystyle,}$

${\ displaystyle l_ {mn_ {m}}}$

${\ displaystyle \}}$

${\ displaystyle \}}$

.

См ниже в качестве примера.

Вычислительная сложность

Важный набор проблем вычислительной сложности включает нахождение присвоений переменным булевой формулы, выраженной в конъюнктивной нормальной форме, таким образом, чтобы формула была истинной. Проблема k -SAT - это проблема нахождения удовлетворительного присваивания булевой формуле, выраженной в CNF, в которой каждая дизъюнкция содержит не более k переменных. 3-SAT является NP-полной (как и любая другая задача k -SAT с k > 2), в то время как 2-SAT, как известно, имеет решения за полиномиальное время . Как следствие, задача преобразования формулы в ДНФ с сохранением выполнимости является NP-трудной ; в общем , преобразование в CNF с сохранением достоверности также является NP-трудным; следовательно, преобразование с сохранением эквивалентности в DNF или CNF снова является NP-трудным.

Типичные проблемы в этом случае связаны с формулами в "3CNF": конъюнктивная нормальная форма с не более чем тремя переменными на конъюнкт. Примеры таких формул, встречающихся на практике, могут быть очень большими, например, со 100 000 переменных и 1 000 000 конъюнктов.

Формула в КНФ может быть преобразована в equisatisfiable формулы в « K CNF» (для к ≥3) путем замены каждого конъюнкт с более чем K переменных двумя конъюнктов и с Z новой переменной, и повторяя так часто , как это необходимо. ${\ Displaystyle X_ {1} \ vee \ cdots \ vee X_ {k} \ vee \ cdots \ vee X_ {n}}$${\ Displaystyle X_ {1} \ vee \ cdots \ vee X_ {k-1} \ vee Z}$${\ displaystyle \ neg Z \ vee X_ {k} \ cdots \ vee X_ {n}}$

Преобразование из логики первого порядка

Чтобы преобразовать логику первого порядка в CNF:

1. Преобразовать в нормальную форму отрицания .
   1. Устранение последствий и эквивалентностей: неоднократно заменять на ; заменить на . В конце концов, это устранит все вхождения и .${\ Displaystyle P \ rightarrow Q}$${\ displaystyle \ lnot P \ lor Q}$${\ displaystyle P \ leftrightarrow Q}$${\ Displaystyle (п \ лор \ lnot Q) \ земля (\ lnot P \ lor Q)}$${\ displaystyle \ rightarrow}$${\ displaystyle \ leftrightarrow}$
   2. Переместите НЕ внутрь, многократно применяя закон Де Моргана . В частности, заменить на ; заменить на ; и заменить на ; заменить на ; с . После этого a может стоять только непосредственно перед предикатным символом.${\ Displaystyle \ lnot (п \ лор Q)}$${\ Displaystyle (\ lnot P) \ земля (\ lnot Q)}$${\ Displaystyle \ lnot (П \ земля Q)}$${\ Displaystyle (\ lnot P) \ lor (\ lnot Q)}$${\ Displaystyle \ lnot \ lnot P}$${\ displaystyle P}$${\ Displaystyle \ lnot (\ forall xP (x))}$${\ Displaystyle \ существует х \ lnot P (x)}$${\ Displaystyle \ lnot (\ существует xP (x))}$${\ Displaystyle \ forall x \ lnot P (x)}$${\ Displaystyle \ lnot}$
2. Стандартизируйте переменные
   1. Для предложений, например, которые используют одно и то же имя переменной дважды, измените имя одной из переменных. Это позволяет избежать путаницы при отбрасывании кванторов. Например, переименован в .${\ Displaystyle (\ forall xP (x)) \ lor (\ существует xQ (x))}$${\ Displaystyle \ forall x [\ существует y \ mathrm {Animal} (y) \ land \ lnot \ mathrm {Loves} (x, y)] \ lor [\ существует y \ mathrm {Loves} (y, x)] }$${\ Displaystyle \ forall x [\ существует y \ mathrm {Animal} (y) \ land \ lnot \ mathrm {Loves} (x, y)] \ lor [\ exists z \ mathrm {Loves} (z, x)] }$
3. Сколемизируйте заявление
   1. Переместить кванторы наружу: повторно заменить на ; заменить на ; заменить на ; заменить на . Эти замены сохраняют эквивалентность, поскольку предыдущий шаг стандартизации переменных гарантировал, что этого не произойдет в . После этих замен, квантор может иметь место только в начальном префиксе формулы, но никогда не Внутри , или .${\ Displaystyle P \ земля (\ forall xQ (x))}$${\ Displaystyle \ forall х (п \ земля Q (х))}$${\ Displaystyle P \ lor (\ forall xQ (x))}$${\ Displaystyle \ forall х (п \ лор Q (х))}$${\ Displaystyle P \ земля (\ существует xQ (x))}$${\ Displaystyle \ существует х (п \ земля Q (х))}$${\ Displaystyle P \ lor (\ существует xQ (x))}$${\ Displaystyle \ существует х (п \ лор Q (х))}$${\ displaystyle x}$${\ displaystyle P}$${\ Displaystyle \ lnot}$${\ displaystyle \ land}$${\ Displaystyle \ lor}$
   2. Неоднократно заменяйте на , где - новый символ функции, так называемая « сколемская функция ». Это единственный шаг, который сохраняет только выполнимость, а не эквивалентность. Он устраняет все экзистенциальные кванторы.${\ Displaystyle \ forall x_ {1} \ ldots \ forall x_ {n} \; \ существует y \; P (y)}$${\ Displaystyle \ forall x_ {1} \ ldots \ forall x_ {n} \; P (f (x_ {1}, \ ldots, x_ {n}))}$${\ displaystyle f}$${\ displaystyle n}$
4. Отбросьте все универсальные кванторы.
5. Распределите ИЛИ внутрь по И: несколько раз замените на .${\ Displaystyle P \ lor (Q \ земля R)}$${\ Displaystyle (P \ lor Q) \ земля (P \ lor R)}$

В качестве примера формула «Любой, кто любит всех животных, в свою очередь, кого-то любит» преобразуется в CNF (а затем в форму предложения в последней строке) следующим образом (выделение правила замены заменяется переиндексом в ): ${\ displaystyle {\ color {красный} {\ text {красный}}}}$

${\ displaystyle \ forall x}$

${\ displaystyle (}$

${\ displaystyle \ forall y}$

${\ displaystyle \ mathrm {животное} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ color {красный} \ rightarrow}$

${\ displaystyle \ mathrm {любит} (х,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ rightarrow}$

${\ displaystyle (}$

${\ Displaystyle \ существует}$

${\ displaystyle y}$

${\ displaystyle \ mathrm {любит} (}$

${\ displaystyle y}$

${\ displaystyle, x)}$

${\ displaystyle)}$

${\ displaystyle \ forall x}$

${\ displaystyle (}$

${\ displaystyle \ forall y}$

${\ Displaystyle \ lnot}$

${\ displaystyle \ mathrm {животное} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ Displaystyle \ lor}$

${\ displaystyle \ mathrm {любит} (х,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ color {красный} \ rightarrow}$

${\ displaystyle (}$

${\ Displaystyle \ существует}$

${\ displaystyle y}$

${\ displaystyle \ mathrm {любит} (}$

${\ displaystyle y}$

${\ displaystyle, x)}$

${\ displaystyle)}$

на 1,1

${\ displaystyle \ forall x}$

${\ displaystyle \ color {красный} \ lnot}$

${\ displaystyle (}$

${\ displaystyle {\ color {красный} {\ forall y}}}$

${\ Displaystyle \ lnot}$

${\ displaystyle \ mathrm {животное} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ Displaystyle \ lor}$

${\ displaystyle \ mathrm {любит} (х,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ Displaystyle \ lor}$

${\ displaystyle (}$

${\ Displaystyle \ существует}$

${\ displaystyle y}$

${\ displaystyle \ mathrm {любит} (}$

${\ displaystyle y}$

${\ displaystyle, x)}$

${\ displaystyle)}$

на 1,1

${\ displaystyle \ forall x}$

${\ displaystyle (}$

${\ Displaystyle \ существует у}$

${\ displaystyle \ color {красный} \ lnot}$

${\ displaystyle (}$

${\ Displaystyle \ lnot}$

${\ displaystyle \ mathrm {животное} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ color {красный} \ lor}$

${\ displaystyle \ mathrm {любит} (х,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ Displaystyle \ lor}$

${\ displaystyle (}$

${\ Displaystyle \ существует}$

${\ displaystyle y}$

${\ displaystyle \ mathrm {любит} (}$

${\ displaystyle y}$

${\ displaystyle, x)}$

${\ displaystyle)}$

на 1,2

${\ displaystyle \ forall x}$

${\ displaystyle (}$

${\ Displaystyle \ существует у}$

${\ displaystyle \ color {красный} \ lnot}$

${\ displaystyle \ color {красный} \ lnot}$

${\ displaystyle \ mathrm {животное} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ land}$

${\ Displaystyle \ lnot}$

${\ displaystyle \ mathrm {любит} (х,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ Displaystyle \ lor}$

${\ displaystyle (}$

${\ Displaystyle \ существует}$

${\ displaystyle y}$

${\ displaystyle \ mathrm {любит} (}$

${\ displaystyle y}$

${\ displaystyle, x)}$

${\ displaystyle)}$

на 1,2

${\ displaystyle \ forall x}$

${\ displaystyle (}$

${\ displaystyle {\ color {красный} {\ существует y}}}$

${\ displaystyle \ mathrm {животное} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ land}$

${\ Displaystyle \ lnot}$

${\ displaystyle \ mathrm {любит} (х,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ Displaystyle \ lor}$

${\ displaystyle (}$

${\ Displaystyle \ цвет {красный} \ существует}$

${\ displaystyle \ color {красный} y}$

${\ displaystyle \ mathrm {любит} (}$

${\ displaystyle y}$

${\ displaystyle, x)}$

${\ displaystyle)}$

на 1,2

${\ displaystyle \ forall x}$

${\ displaystyle (}$

${\ Displaystyle \ существует у}$

${\ displaystyle \ mathrm {животное} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ land}$

${\ Displaystyle \ lnot}$

${\ displaystyle \ mathrm {любит} (х,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ color {красный} \ lor}$

${\ displaystyle (}$

${\ Displaystyle \ цвет {красный} \ существует}$

${\ displaystyle \ color {красный} z}$

${\ displaystyle \ mathrm {любит} (}$

${\ displaystyle z}$

${\ displaystyle, x)}$

${\ displaystyle)}$

на 2

${\ displaystyle \ forall x}$

${\ Displaystyle \ существует z}$

${\ displaystyle (}$

${\ displaystyle {\ color {красный} {\ существует y}}}$

${\ displaystyle \ mathrm {животное} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ land}$

${\ Displaystyle \ lnot}$

${\ displaystyle \ mathrm {любит} (х,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ color {красный} \ lor}$

${\ displaystyle \ mathrm {любит} (}$

${\ displaystyle z}$

${\ displaystyle, x)}$

на 3,1

${\ displaystyle \ forall x}$

${\ displaystyle {\ color {красный} {\ существует z}}}$

${\ Displaystyle \ существует у}$

${\ displaystyle (}$

${\ displaystyle \ mathrm {животное} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ land}$

${\ Displaystyle \ lnot}$

${\ displaystyle \ mathrm {любит} (х,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ Displaystyle \ lor}$

${\ displaystyle \ mathrm {любит} (}$

${\ displaystyle z}$

${\ displaystyle, x)}$

на 3,1

${\ displaystyle \ forall x}$

${\ displaystyle {\ color {красный} {\ существует y}}}$

${\ displaystyle (}$

${\ displaystyle \ mathrm {животное} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ land}$

${\ Displaystyle \ lnot}$

${\ displaystyle \ mathrm {любит} (х,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ Displaystyle \ lor}$

${\ displaystyle \ mathrm {любит} (}$

${\ displaystyle g (x)}$

${\ displaystyle, x)}$

на 3,2

${\ displaystyle (}$

${\ displaystyle \ mathrm {животное} (}$

${\ displaystyle f (x)}$

${\ displaystyle)}$

${\ displaystyle \ color {красный} \ land}$

${\ Displaystyle \ lnot}$

${\ displaystyle \ mathrm {любит} (х,}$

${\ displaystyle f (x)}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ color {красный} \ lor}$

${\ displaystyle \ mathrm {любит} (}$

${\ displaystyle g (x)}$

${\ displaystyle, x)}$

по 4

${\ displaystyle (}$

${\ displaystyle \ mathrm {животное} (}$

${\ displaystyle f (x)}$

${\ displaystyle)}$

${\ displaystyle \ color {красный} \ lor}$

${\ displaystyle \ mathrm {любит} (}$

${\ displaystyle g (x)}$

${\ displaystyle, x)}$

${\ displaystyle)}$

${\ displaystyle \ color {красный} \ land}$

${\ displaystyle (}$

${\ Displaystyle \ lnot \ mathrm {любит} (х, е (х))}$

${\ displaystyle \ color {красный} \ lor}$

${\ Displaystyle \ mathrm {любит} (г (х), х)}$

${\ displaystyle)}$

на 5

${\ displaystyle \ {}$

${\ displaystyle \ {}$

${\ displaystyle \ mathrm {животное} (}$

${\ displaystyle f (x)}$

${\ displaystyle)}$

${\ displaystyle,}$

${\ displaystyle \ mathrm {любит} (}$

${\ displaystyle g (x)}$

${\ displaystyle, x)}$

${\ displaystyle \}}$

${\ displaystyle,}$

${\ displaystyle \ {}$

${\ Displaystyle \ lnot \ mathrm {любит} (х, е (х))}$

${\ displaystyle,}$

${\ Displaystyle \ mathrm {любит} (г (х), х)}$

${\ displaystyle \}}$

${\ displaystyle \}}$

( представление статьи )

Неформально функция Сколема может рассматриваться как уступка человеку, которого любит, в то время как порождение животного (если оно есть), которое не любит. Третья последняя строка снизу читается как « не любит животное , иначе его любит » . ${\ displaystyle g (x)}$${\ displaystyle x}$${\ displaystyle f (x)}$${\ displaystyle x}$${\ displaystyle x}$${\ displaystyle f (x)}$${\ displaystyle x}$${\ displaystyle g (x)}$

Вторая последняя строка сверху - это CNF. ${\ Displaystyle (\ mathrm {Животное} (е (х)) \ лор \ mathrm {любит} (г (х), х)) \ земля (\ lnot \ mathrm {любит} (х, е (х)) \ lor \ mathrm {любит} (g (x), x))}$

Примечания

Смотрите также

• Алгебраическая нормальная форма
• Дизъюнктивная нормальная форма
• Оговорка о роге
• Алгоритм Куайна – Маккласки

использованная литература

• Дж. Элдон Уайтситт (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, показывающий используемые законы