Представяне на безкванторни формули в конюнктивна нормална форма

Представяне на безкванторни формули в конюнктивна нормална форма

казваме, че една формула е елементарна дизюнкция, ако тя се представя във вида L₁  L₂  …  L_n, n  0, където L₁, L₂, …, L_n са литерали;

казваме, че една формула е в конюнктивна нормална форма, ако тя има вида D₁ & D₂ & … & D_n, n  0, където D₁, D₂, …, D_n са елементарни дизюнкции;

за всяка безкванторна формула F, която не е атомарна дефинираме преработено отрицание -F:

ако F = true, -F = fail;

ако F = fail, -F = true;

ако F = G, -F = G;

ако F = G₁  G₂  …  G_n, n > 1, -F = G₁ & G₂ & … & G_n;

ако F = G₁ & G₂ & … & G_n, n > 1, -F = G₁  G₂  …  G_n;
ясно е, че за всяка формула F, която не е атомарна е изпълнено:

F  -F;
за всяка безкванторна формула F дефинираме заменящо множество на F:

ако F е елементарна дизюнкция, заменящото множество на F е { F};

нека F не е елементарна дизюнкция; тогава F може да се представи във вида F = F₁  F₂  …  F_n, където n > 0, тъй като fail е елементарна дизюнкция; при това, ако n = 1 можем да считаме, че F₁ не е дизюнкция с повече от един член;

тъй като F не е елементарна дизюнкция,

то F_i не е литерал за някое i  { 1, 2, …, n };

ако F_i = true, заменящото множество на F е ;

ако F_i = fail, заменящото множество на F е

{ F₁  …  F_i-1  F_i+1  …  F_n}; при това n > 1, тъй като F не е елементарна дизюнкция;

ако F_i = G, заменящото множество на F е

{ F₁  …  F_i-1  -G  F_i+1  …  F_n}; при това G не е атомарна формула, тъй като F_i не е литерал, така че -G е дефинирано;

ако F_i = G₁ & G₂ & … & G_k, k > 1, заменящото множество на F е

{ F₁  …  F_i-1  G_j  F_i+1  …  F_n| j = 1, 2, …, k };

ако F_i = G₁  G₂  …  G_k, k > 1, заменящото множество на F е

{ F₁  …  F_i-1  G₁  G₂  …  G_k  F_i+1  …  F_n}; при това n > 1, тъй като при n = 1 имаме, че F₁ не е дизюнкция с повече от един член;
съвсем лесно се вижда, че ако F е безкванторна формула, конюнкцията на елементите на кое да е заменящо множество на F е еквивалентна на F; например, в горните означения, ще покажем това в случая F_i = G₁ & G₂ & … & G_k, k > 1; заменящото множество на F е { F₁  …  F_i-1  G_j  F_i+1  …  F_n| j = 1, 2, …, k };

нека S е структура, v е оценка на променливите в S;

да предположим, че F ^{S, v} = 1; тогава F_j ^{S, v} = 1 за някое

j  { 1, 2, …, n }; нека j  i; тогава формулите в заменящото множество са дизюнкции, които имат член F_j, така че тези формули са вярни в S при оценката v  конюнкцията им е вярна в S при оценката v; ако j = i, то (G₁ & G₂ & … & G_k)^{S, v} = 1 

G₁, G₂, …, G_k са вярни в S при оценката v; тогава формулите в заменящото множество са дизюнкции, които имат член G_m за някое m  { 1, 2, …, k }, така че тези формули са вярни в S при оценката v  конюнкцията им е вярна в S при оценката v;

обратно, нека конюнкцията на формулите в заменящото множество е вярна в S при оценката v; тогава тези формули са вярни в S при оценката v и тъй като тези формули са дизюнкции, то във всяка от тях поне един член е верен в S при оценката v;

ако за някоя формула този член е F_j за някое

j  { 1, …, i-1, i+1, …, n }  F е вярна в S при оценката v, тъй като F е дизюнкция, която има член F_j; ако за всички формули този член е G_m, m = 1, 2, …, k, то F_i = G₁ & G₂ & … & G_k е вярна в S при оценката v  F е вярна в S при оценката v, тъй като F е дизюнкция, която има член F_i;

Доказателство: нека F е безкванторна формула;

ще посочим алгоритъм, по който се построява еквивалентна на F формула в конюнктивна нормална форма;

1. 
   M = { F };
   
2. 
   за всяка формула от множеството M образуваме заменящо множество; нека M е обединението на получените заменящи множества;
   
3. 
   ако M се състои само от елементарни дизюнкции, към 4.; иначе M = M, към 2.;
   
4. 
   нека G е конюнкцията на всички формули от M; търсената формула е G; край;
   

ясно е, че G е в конюнктивна нормална форма, тъй като на последната стъпка M се състои само от елементарни дизюнкции;

на всяка стъпка, конюнкцията на формулите от M е еквивалентна на формулата F съгласно горните съображения, така че на последната стъпка получаваме, че F  G;

не е трудно да се покаже, че алгоритъмът завършва след краен брой стъпки – достатъчно е да се дефинира по подходящ начин сложност на формула и да се покаже, че на всяка стъпка от алгоритъма сложността на формулите в M строго намалява, докато те не се преобразуват в елементарни дизюнкции;