WikiDer > Конъюнктивті қалыпты форма

Жылы Логикалық логика, а формула ішінде конъюнктивті қалыпты форма (CNF) немесе сөйлем қалыпты формасы егер бұл а конъюнкция бір немесе бірнеше тармақтар, мұндағы сөйлем а дизъюнкция туралы литералдар; басқаша айтқанда, бұл а қосындылардың көбейтіндісі немесе ЖӘНЕ ОР-лар. Сияқты канондық қалыпты форма, бұл пайдалы автоматтандырылған теорема және тізбек теориясы.

Литералдардың барлық конъюнкциялары және литералдардың барлық дизъюнкциялары CNF-де орналасқан, өйткені оларды сәйкесінше бір әріптік сөйлемдердің және бірыңғай сөйлемнің конъюнкциялары ретінде қарастыруға болады. Сияқты дизъюнктивті қалыпты форма (DNF), формула құрамында CNF формуласы болуы мүмкін жалғыз қосылғыш және, немесе, және емес. Not операторы тек сөзбе-сөздің бөлігі ретінде қолданыла алады, демек ол тек a-дан бұрын болуы мүмкін пропозициялық айнымалы немесе а предикат белгісі.

Автоматтандырылған теореманы дәлелдеу кезінде «сөйлем қалыпты формасы«жиі тар мағынада қолданылады, яғни CNF формуласының литералдар жиынтығы ретінде белгілі бір көрінісін білдіреді.

Мысалдар және мысалдар емес

A, B, C, D, E және F айнымалыларындағы барлық келесі формулалар конъюнктивті қалыпты формада:

• ${ displaystyle (A lor neg B lor neg C) land ( neg D lor E lor F)}$
• ${ displaystyle (A lor B) land C}$
• ${ displaystyle A lor B}$
• ${ displaystyle A}$

Үшінші формула конъюнктивті қалыпты формада, өйткені ол тек бір ғана қосылғышпен, яғни сөйлеммен «конъюнкция» ретінде қарастырылады ${ displaystyle A lor B}$.Айтпақшы, соңғы екі формула да дизъюнктивті қалыпты форма.

Келесі формулалар емес конъюнктивті қалыпты түрінде:

• ${ displaystyle neg (B lor C)}$, НЕМЕСЕ ЕМЕС ішінде орналастырылғандықтан
• ${ displaystyle (A land B) lor C}$
• ${ displaystyle A land (B lor (D land E))}$, ЖӘНЕ НЕМЕСЕ ішінде орналасады

Кез-келген формуланы конъюнктивті қалыпты формула түрінде формула түрінде жазуға болады, атап айтқанда бұл жоғарыда аталған үш мысалға қатысты емес; олар сәйкесінше конъюнктивті қалыпты формадағы келесі үш формулаға тең:

• ${ displaystyle neg B land neg C}$
• ${ displaystyle (A lor C) land (B lor C)}$
• ${ displaystyle A land (B lor D) land (B lor E).}$

CNF-ге конверсия

^[1]Әрқайсысы ұсыныстық формула түрлендіруге болады балама 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}) wedge (Y_ {1} vee X_ {2} vee cdots vee X_ {n}) сына (X_ {1} vee Y_ {2} vee cdots vee X_ {n}) wedge (Y_ {1} vee Y_ {2} vee cdots vee X_ {n}) wedge cdots wedge (Y_ {1} vee Y_ {2} vee cdots vee Y_ {n}).}$

Бұл формула құрамында ${ displaystyle 2 ^ {n}}$ тармақтар; әрбір сөйлемде екеуі де бар ${ displaystyle X_ {i}}$ немесе ${ displaystyle Y_ {i}}$ әрқайсысы үшін ${ displaystyle i}$.

Сақтау арқылы мөлшердің экспоненциалды ұлғаюына жол бермейтін CNF-ге айналу бар қанағаттанушылық гөрі баламалылық.^[2][3] Бұл түрлендірулер формуланың мөлшерін тек сызықтық ұлғайтуға кепілдік береді, бірақ жаңа айнымалыларды енгізеді. Мысалы, жоғарыдағы формуланы айнымалыларды қосу арқылы CNF-ге айналдыруға болады ${ displaystyle Z_ {1}, ldots, Z_ {n}}$ келесідей:

${ displaystyle (Z_ {1} vee cdots vee Z_ {n}) wedge ( neg Z_ {1} vee X_ {1}) wedge ( 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_ {i} vee neg X_ {i} vee neg Y_ {i}}$. Осы тармақтардың көмегімен формула көздейді ${ displaystyle Z_ {i} equiv X_ {i} wedge Y_ {i}}$; бұл формула көбінесе «анықтау» деп саналады ${ displaystyle Z_ {i}}$ үшін атау болу ${ displaystyle X_ {i} wedge 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 }}$

.

Қараңыз төменде мысал үшін.

Есептеудің күрделілігі

Проблемаларының маңызды жиынтығы есептеу күрделілігі логикалық формуланың конъюнктивтік қалыпты формада көрсетілген айнымалыларына формула шындыққа сәйкес келетін тапсырмаларды табуды қамтиды. The к-SAT есебі - бұл әр дизъюнкция ең көп мөлшерде болатын CNF-де көрсетілген буль формуласына қанағаттанарлық тапсырманы табу мәселесі. к айнымалылар. 3-SAT болып табылады NP аяқталды (басқалар сияқты) к- SAT мәселесі к> 2) while 2-SAT шешімдері бар екені белгілі көпмүшелік уақыт.Нәтижесінде,^[4] формуланы а-ға түрлендіру міндеті DNF, қанағаттанушылықты сақтау, болып табылады NP-hard; қосарланған, консервілеу, CNF-ге айналдыру жарамдылық, NP-қатты болып табылады; демек, DNF немесе CNF-ге баламалығын сақтайтын конверсия NP-қиын.

Бұл жағдайда типтік мәселелер «3CNF» формулаларын қамтиды: конъюнктивті қалыпты форма, конъюнкцияда үш айнымалыдан аспайды. Практикада кездесетін осындай формулалардың мысалдары өте үлкен болуы мүмкін, мысалы 100000 айнымалы және 1000000 конъюнктура.

CNF-дегі формуланы «теңдейтін формулаға» айналдыруға боладыкCNF »(үшін к≥3) әрбір жалғаулықты одан әріге ауыстыру арқылы к айнымалылар ${ 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. Түрлендіру теріске шығару қалыпты формасы.
   1. Салдары мен эквиваленттерін алып тастаңыз: бірнеше рет ауыстырыңыз ${ displaystyle P rightarrow Q}$ бірге ${ displaystyle lnot P lor Q}$; ауыстыру ${ displaystyle P leftrightarrow Q}$ бірге ${ displaystyle (P lor lnot Q) land ( lnot P lor Q)}$. Сайып келгенде, бұл барлық жағдайларды жояды ${ displaystyle rightarrow}$ және ${ displaystyle leftrightarrow}$.
   2. Бірнеше рет қолдану арқылы ЕМЕС-терді ішке қарай жылжытыңыз Де Морган заңы. Атап айтқанда, ауыстырыңыз ${ displaystyle lnot (P lor Q)}$ бірге ${ displaystyle ( lnot P) land ( lnot Q)}$; ауыстыру ${ displaystyle lnot (P land Q)}$ бірге ${ displaystyle ( lnot P) lor ( lnot Q)}$; және ауыстырыңыз ${ displaystyle lnot lnot P}$ бірге ${ displaystyle P}$; ауыстыру ${ displaystyle lnot ( forall xP (x))}$ бірге ${ displaystyle бар x l емес P (x)}$; ${ displaystyle lnot ( бар xP (x))}$ бірге ${ displaystyle forall x l емес 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 [ z mathrm {Loves} (z, x)) бар }$.
3. Skolemize мәлімдеме
   1. Сандық белгілерді сыртқа жылжытыңыз: бірнеше рет ауыстырыңыз ${ displaystyle P land ( forall xQ (x))}$ бірге ${ displaystyle forall x (P land Q (x))}$; ауыстыру ${ displaystyle P lor ( forall xQ (x))}$ бірге ${ displaystyle forall x (P lor Q (x))})$; ауыстыру ${ displaystyle P land ( xQ (x) бар)}$ бірге ${ displaystyle бар x (P land Q (x))}$; ауыстыру ${ displaystyle P lor ( xQ (x) бар)}$ бірге ${ displaystyle x (P lor Q (x))} бар$. Бұл алмастырулар эквиваленттілікті сақтайды, өйткені алдыңғы айнымалы стандарттау қадамы оны қамтамасыз етті ${ 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}$-ary функциясы, «деп аталатынсколем функциясы«. Бұл эквиваленттіліктен гөрі қанағаттанушылықты сақтайтын жалғыз қадам. Ол барлық экзистенциалдық кванторларды жояды.
4. Барлық әмбебап кванторларды тастаңыз.
5. ЖӘНЕ-ді AND-ге қарай таратыңыз: бірнеше рет ауыстырыңыз ${ displaystyle P lor (Q land R)}$ бірге ${ displaystyle (P lor Q) land (P lor R)}$.

Мысал ретінде формула айтылады «Барлық жануарларды жақсы көретін адам, өз кезегінде оны жақсы көреді» CNF-ге айналады (және кейіннен) тармақ соңғы жолға) келесі жолмен салыңыз (ауыстыру ережесін бөлектеңіз редекстер жылы ${ displaystyle { color {red} { text {red}}}}$):

${ displaystyle forall x}$

${ displaystyle (}$

${ displaystyle forall y}$

${ displaystyle mathrm {Animal} (}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle color {red}} rightarrow}$

${ displaystyle mathrm {Loves} (x,}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle)}$

${ displaystyle rightarrow}$

${ displaystyle (}$

${ displaystyle бар}$

${ displaystyle y}$

${ displaystyle mathrm {Loves} (}$

${ displaystyle y}$

${ displaystyle, x)}$

${ displaystyle)}$

${ displaystyle forall x}$

${ displaystyle (}$

${ displaystyle forall y}$

${ displaystyle lnot}$

${ displaystyle mathrm {Animal} (}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle lor}$

${ displaystyle mathrm {Loves} (x,}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle)}$

${ displaystyle color {red}} rightarrow}$

${ displaystyle (}$

${ displaystyle бар}$

${ displaystyle y}$

${ displaystyle mathrm {Loves} (}$

${ displaystyle y}$

${ displaystyle, x)}$

${ displaystyle)}$

1.1 бойынша

${ displaystyle forall x}$

${ displaystyle color {red} lnot}$

${ displaystyle (}$

${ displaystyle { color {red} { for all y}}}$

${ displaystyle lnot}$

${ displaystyle mathrm {Animal} (}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle lor}$

${ displaystyle mathrm {Loves} (x,}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle)}$

${ displaystyle lor}$

${ displaystyle (}$

${ displaystyle бар}$

${ displaystyle y}$

${ displaystyle mathrm {Loves} (}$

${ displaystyle y}$

${ displaystyle, x)}$

${ displaystyle)}$

1.1 бойынша

${ displaystyle forall x}$

${ displaystyle (}$

${ displaystyle бар y}$

${ displaystyle color {red} lnot}$

${ displaystyle (}$

${ displaystyle lnot}$

${ displaystyle mathrm {Animal} (}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle color {red}} lor}$

${ displaystyle mathrm {Loves} (x,}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle)}$

${ displaystyle)}$

${ displaystyle lor}$

${ displaystyle (}$

${ displaystyle бар}$

${ displaystyle y}$

${ displaystyle mathrm {Loves} (}$

${ displaystyle y}$

${ displaystyle, x)}$

${ displaystyle)}$

1.2 бойынша

${ displaystyle forall x}$

${ displaystyle (}$

${ displaystyle бар y}$

${ displaystyle color {red} lnot}$

${ displaystyle color {red} lnot}$

${ displaystyle mathrm {Animal} (}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle land}$

${ displaystyle lnot}$

${ displaystyle mathrm {Loves} (x,}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle)}$

${ displaystyle lor}$

${ displaystyle (}$

${ displaystyle бар}$

${ displaystyle y}$

${ displaystyle mathrm {Loves} (}$

${ displaystyle y}$

${ displaystyle, x)}$

${ displaystyle)}$

1.2

${ displaystyle forall x}$

${ displaystyle (}$

${ displaystyle { color {red} { y}}} бар$

${ displaystyle mathrm {Animal} (}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle land}$

${ displaystyle lnot}$

${ displaystyle mathrm {Loves} (x,}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle)}$

${ displaystyle lor}$

${ displaystyle (}$

${ displaystyle color {red}} бар}$

${ displaystyle color {red} y}$

${ displaystyle mathrm {Loves} (}$

${ displaystyle y}$

${ displaystyle, x)}$

${ displaystyle)}$

1.2

${ displaystyle forall x}$

${ displaystyle (}$

${ displaystyle бар y}$

${ displaystyle mathrm {Animal} (}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle land}$

${ displaystyle lnot}$

${ displaystyle mathrm {Loves} (x,}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle)}$

${ displaystyle color {red}} lor}$

${ displaystyle (}$

${ displaystyle color {red}} бар}$

${ displaystyle color {red} z}$

${ displaystyle mathrm {Loves} (}$

${ displaystyle z}$

${ displaystyle, x)}$

${ displaystyle)}$

2

${ displaystyle forall x}$

${ displaystyle бар z}$

${ displaystyle (}$

${ displaystyle { color {red} { y}}} бар$

${ displaystyle mathrm {Animal} (}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle land}$

${ displaystyle lnot}$

${ displaystyle mathrm {Loves} (x,}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle)}$

${ displaystyle color {red}} lor}$

${ displaystyle mathrm {Loves} (}$

${ displaystyle z}$

${ displaystyle, x)}$

3.1 бойынша

${ displaystyle forall x}$

${ displaystyle { color {red} { z}}} бар$

${ displaystyle бар y}$

${ displaystyle (}$

${ displaystyle mathrm {Animal} (}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle land}$

${ displaystyle lnot}$

${ displaystyle mathrm {Loves} (x,}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle)}$

${ displaystyle lor}$

${ displaystyle mathrm {Loves} (}$

${ displaystyle z}$

${ displaystyle, x)}$

3.1 бойынша

${ displaystyle forall x}$

${ displaystyle { color {red} { y}}} бар$

${ displaystyle (}$

${ displaystyle mathrm {Animal} (}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle land}$

${ displaystyle lnot}$

${ displaystyle mathrm {Loves} (x,}$

${ displaystyle y}$

${ displaystyle)}$

${ displaystyle)}$

${ displaystyle lor}$

${ displaystyle mathrm {Loves} (}$

${ displaystyle g (x)}$

${ displaystyle, x)}$

3.2

${ displaystyle (}$

${ displaystyle mathrm {Animal} (}$

${ displaystyle f (x)}$

${ displaystyle)}$

${ displaystyle color {red} land}$

${ displaystyle lnot}$

${ displaystyle mathrm {Loves} (x,}$

${ displaystyle f (x)}$

${ displaystyle)}$

${ displaystyle)}$

${ displaystyle color {red}} lor}$

${ displaystyle mathrm {Loves} (}$

${ displaystyle g (x)}$

${ displaystyle, x)}$

4-ке

${ displaystyle (}$

${ displaystyle mathrm {Animal} (}$

${ displaystyle f (x)}$

${ displaystyle)}$

${ displaystyle color {red}} lor}$

${ displaystyle mathrm {Loves} (}$

${ displaystyle g (x)}$

${ displaystyle, x)}$

${ displaystyle)}$

${ displaystyle color {red} land}$

${ displaystyle (}$

${ displaystyle lnot mathrm {Сүйеді} (x, f (x))}$

${ displaystyle color {red}} lor}$

${ displaystyle mathrm {Сүйеді} (g (x), x)}$

${ displaystyle)}$

5-ке

${ displaystyle {}$

${ displaystyle {}$

${ displaystyle mathrm {Animal} (}$

${ displaystyle f (x)}$

${ displaystyle)}$

${ displaystyle,}$

${ displaystyle mathrm {Loves} (}$

${ displaystyle g (x)}$

${ displaystyle, x)}$

${ displaystyle }}$

${ displaystyle,}$

${ displaystyle {}$

${ displaystyle lnot mathrm {Сүйеді} (x, f (x))}$

${ displaystyle,}$

${ displaystyle mathrm {Сүйеді} (g (x), x)}$

${ displaystyle }}$

${ displaystyle }}$

(тармақ өкілдік)

Бейресми түрде сколем функциясы ${ displaystyle g (x)}$ адамға қолғабыс ету деп ойлауға болады ${ displaystyle x}$ сүйеді, ал ${ displaystyle f (x)}$ жануарды береді (егер бар болса) ${ displaystyle x}$ сүймейді. Төмендегі 3-ші соңғы жол келесідей оқылады "${ displaystyle x}$ жануарды жақсы көрмейді ${ displaystyle f (x)}$, немесе басқа ${ displaystyle x}$ сүйеді ${ displaystyle g (x)}$".

Жоғарыдан 2-ші соңғы жол, ${ displaystyle ( mathrm {Animal} (f (x)) lor mathrm {Loves} (g (x), x)) land ( lnot mathrm {Loves} (x, f (x))) lor mathrm {Сүйеді} (g (x), x))}$, бұл CNF.

Ескертулер

Сондай-ақ қараңыз

• Алгебралық қалыпты форма
• Дизъюнктивті қалыпты форма
• Мүйіз туралы сөйлем
• Квин-Макклук алгоритмі

Әдебиеттер тізімі

• Дж.Элдон Уайтситт (24 мамыр 2012). Буль алгебрасы және оның қолданылуы. Courier Corporation. ISBN 978-0-486-15816-7.
• Ханс Клейн Бюнинг; Теодор Леттманн (28 тамыз 1999). Ұсыныс логикасы: дедукция және алгоритмдер. Кембридж университетінің баспасы. ISBN 978-0-521-63017-7.
• Пол Джексон, Даниэль Шеридан: Логикалық тізбектерге арналған түрлендірулер. Хольгер Х. Хоос, Дэвид Г. Митчелл (Ред.): Қанықтылықты тестілеудің теориясы мен қолданылуы, 7 Халықаралық конференция, SAT 2004, Ванкувер, BC, Канада, 2004 ж. 10-13 мамыр, қайта қаралған таңдамалы мақалалар. Информатикадағы дәрістер 3542, Springer 2005, 183–198 бб
• Г.С. Цейтин: Пропозициялық есептеудегі туындының күрделілігі туралы. С: Слисенко, А.О. (ред.) Конструктивті математика және математикалық логика құрылымдары, II бөлім, математикадан семинарлар (орыс тілінен аударылған), 115-125 бб. Стеклов атындағы математикалық институт (1968)

Сыртқы сілтемелер

• «Конъюнктивті қалыпты форма», Математика энциклопедиясы, EMS Press, 2001 [1994]
• CNF және DNF түрлендіруге арналған Java апплеті, қолданылған заңдарды көрсетеді