الصيغة العادية للوصل

الخوارزمية لحساب مكافئ صيغة CNF لصيغة اقتراحية معينة${\displaystyle \phi }$يبني على${\displaystyle \lnot \phi }$في الصيغة الطبيعية المنفصلة (DNF) : الخطوة 1. ^{[ 2 ]} ثم${\displaystyle \lnot \phi _{DNF}}$يتم تحويلها إلى${\displaystyle \phi _{CNF}}$عن طريق تبديل AND مع OR والعكس مع نفي جميع القيم الحرفية. قم بإزالة الكل${\displaystyle \lnot \lnot }$[ ^{1 ]​}

التحويل بالوسائل الدلالية

يمكن اشتقاق صيغة CNF مكافئة لصيغة ما من جدول الحقيقة الخاص بها . لننظر مرة أخرى إلى الصيغة $${\displaystyle \phi =((\lnot (p\land q))\leftrightarrow (\lnot r\uparrow (p\oplus q)))}$$[ ^{5 ]​}

جدول الحقيقة المقابل هو

${\displaystyle p}$	${\displaystyle q}$	${\displaystyle r}$		${\displaystyle (}$	${\displaystyle \lnot }$	${\displaystyle (p\land q)}$	${\displaystyle )}$	${\displaystyle \leftrightarrow }$	${\displaystyle (}$	${\displaystyle \lnot r}$	${\displaystyle \uparrow }$	${\displaystyle (p\oplus q)}$	${\displaystyle )}$
تي	تي	تي			F	تي		F		F	تي	F
تي	تي	F			F	تي		F		تي	تي	F
تي	F	تي			تي	F		تي		F	تي	تي
تي	F	F			تي	F		F		تي	F	تي
F	تي	تي			تي	F		تي		F	تي	تي
F	تي	F			تي	F		F		تي	F	تي
F	F	تي			تي	F		تي		F	تي	F
F	F	F			تي	F		تي		تي	تي	F

مكافئ CNF لـ${\displaystyle \phi }$يكون $${\displaystyle (\lnot p\lor \lnot q\lor \lnot r)\land (\lnot p\lor \lnot q\lor r)\land (\lnot p\lor q\lor r)\land (p\lor \lnot q\lor r)}$$

يعكس كل فصل تعيينًا للمتغيرات التي${\displaystyle \phi }$ إذا كانت قيمة المتغير في مثل هذه الحالة F (خطأ).${\displaystyle V}$

• إذا كانت القيمة T (صحيحة)، فسيتم تعيين القيمة الحرفية إلى${\displaystyle \lnot V}$في الانفصال،
• إذا كانت القيمة F (خطأ)، فسيتم تعيين القيمة الحرفية إلى${\displaystyle V}$في الانفصال.

بما أن جميع الصيغ المنطقية قابلة للتحويل إلى صيغة مكافئة في الصيغة الاقترانية العادية، فإن البراهين غالبًا ما تُبنى على افتراض أن جميع الصيغ هي صيغة اقترانية عادية. مع ذلك، في بعض الحالات، قد يؤدي هذا التحويل إلى الصيغة الاقترانية العادية إلى تضخم هائل في الصيغة. على سبيل المثال، عند ترجمة الصيغة غير الاقترانية العادية

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

ينتج عن تحويل CNF تركيبة مع${\displaystyle 2^{n}}$بنود:

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

تحتوي كل جملة على إما${\displaystyle X_{i}}$أو${\displaystyle Y_{i}}$لكل${\displaystyle i}$.

توجد تحويلات إلى صيغة CNF تتجنب الزيادة الأسية في الحجم عن طريق الحفاظ على قابلية الإرضاء بدلاً من التكافؤ . ^{[ 6 ] [ 7 ]} تضمن هذه التحويلات زيادة خطية فقط في حجم الصيغة، ولكنها تُدخل متغيرات جديدة. على سبيل المثال، يمكن تحويل الصيغة أعلاه إلى صيغة CNF بإضافة متغيرات.${\displaystyle Z_{1},\ldots ,Z_{n}}$على النحو التالي:

$${\displaystyle (Z_{1}\vee \ldots \vee Z_{n})\wedge (\neg Z_{1}\vee X_{1})\wedge (\neg Z_{1}\vee Y_{1})\wedge \ldots \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: ^{[ 12 ]}

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 \exists x\lnot P(x)}$؛${\displaystyle \lnot (\exists xP(x))}$مع${\displaystyle \forall x\lnot P(x)}$بعد ذلك،${\displaystyle \lnot }$قد يحدث ذلك فقط قبل رمز المسند مباشرة.
2. توحيد المتغيرات
   1. بالنسبة للجمل مثل${\displaystyle (\forall xP(x))\lor (\exists xQ(x))}$في حال استخدام نفس اسم المتغير مرتين، قم بتغيير اسم أحد المتغيرين. هذا يمنع حدوث لبس لاحقاً عند حذف المحددات الكمية. على سبيل المثال،${\displaystyle \forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists y\mathrm {Loves} (y,x)]}$تمت إعادة تسميته إلى${\displaystyle \forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists z\mathrm {Loves} (z,x)]}$.
3. سكولمايز البيان
   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 (\exists xQ(x))}$مع${\displaystyle \exists x(P\land Q(x))}$؛ يستبدل${\displaystyle P\lor (\exists xQ(x))}$مع${\displaystyle \exists x(P\lor Q(x))}$تحافظ هذه الاستبدالات على التكافؤ، لأن خطوة توحيد المتغيرات السابقة ضمنت ذلك.${\displaystyle x}$لا يحدث في${\displaystyle P}$بعد هذه الاستبدالات، قد يظهر المُكمِّم فقط في البادئة الأولية للصيغة، ولكن ليس داخلها أبدًا.${\displaystyle \lnot }$،${\displaystyle \land }$، أو${\displaystyle \lor }$.
   2. استبدل بشكل متكرر${\displaystyle \forall x_{1}\ldots \forall x_{n}\;\exists 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. قم بتوزيع عمليات OR داخليًا على عمليات 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 \exists }$

${\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 \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

بمقدار 1.1

${\displaystyle \forall x}$

${\displaystyle \color {red}\lnot }$

${\displaystyle (}$

${\displaystyle {\color {red}{\forall y}}}$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \lor }$

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

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

بمقدار 1.1

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists 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 \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

بمقدار 1.2

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists 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 \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

بمقدار 1.2

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle {\color {red}{\exists 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}\exists }$

${\displaystyle \color {red}y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

بمقدار 1.2

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists 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}\exists }$

${\displaystyle \color {red}z}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle z}$

${\displaystyle ,x)}$

${\displaystyle )}$

بواسطة 2

${\displaystyle \forall x}$

${\displaystyle \exists z}$

${\displaystyle (}$

${\displaystyle {\color {red}{\exists 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}{\exists z}}}$

${\displaystyle \exists 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}{\exists 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)}$

بحلول الساعة الرابعة

${\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 {Loves} (x,f(x))}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (g(x),x)}$

${\displaystyle )}$

بحلول الساعة الخامسة

${\displaystyle \{}$

${\displaystyle \{}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle ,}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

${\displaystyle \}}$

${\displaystyle ,}$

${\displaystyle \{}$

${\displaystyle \lnot \mathrm {Loves} (x,f(x))}$

${\displaystyle ,}$

${\displaystyle \mathrm {Loves} (g(x),x)}$

${\displaystyle \}}$

${\displaystyle \}}$

( تمثيل البند )

بشكل غير رسمي، دالة سكوليم${\displaystyle g(x)}$يمكن اعتبار ذلك بمثابة تنازل من قبل الشخص الذي${\displaystyle x}$محبوب، بينما${\displaystyle f(x)}$ينتج عنه الحيوان (إن وجد) الذي${\displaystyle x}$لا يحب. ثم يُقرأ السطر الثالث من الأسفل على النحو التالي: "${\displaystyle x}$لا يحب الحيوان${\displaystyle f(x)}$أو غير ذلك${\displaystyle x}$محبوب من قبل${\displaystyle g(x)}$" .

السطر قبل الأخير من الأعلى،${\displaystyle (\mathrm {Animal} (f(x))\lor \mathrm {Loves} (g(x),x))\land (\lnot \mathrm {Loves} (x,f(x))\lor \mathrm {Loves} (g(x),x))}$، هو الصيغة المشتركة للصيغة.