الصيغة الطبيعية للنفي

في المنطق الرياضي ، تكون الصيغة في صيغة النفي العادية ( NNF ) إذا كان عامل النفي (${\displaystyle \lnot }$لا يتم تطبيق عامل النفي (، ) إلا على المتغيرات، وعوامل العطف المنطقية الأخرى المسموح بها هي عوامل العطف (${\displaystyle \land }$، و ) وفصل (${\displaystyle \lor }$، أو ).

لا يُعدّ الشكل الطبيعي للنفي شكلاً قانونياً : على سبيل المثال،${\displaystyle a\land (b\lor \lnot c)}$و${\displaystyle (a\land b)\lor (a\land \lnot c)}$متكافئتان، وكلاهما في صيغة النفي العادية.

فيما يلي قواعد نحوية خالية من السياق لصيغة NNF :

NNF	${\displaystyle \to }$	حرفيًا
		${\displaystyle \mid \quad }$( NNF)${\displaystyle \,\land \,}$NNF  )
		${\displaystyle \mid \quad }$( NNF)${\displaystyle \,\lor \,}$NNF  )
حرفيًا	${\displaystyle \to }$	عامل
		${\displaystyle \mid \quad \neg \,}$عامل

حيث يمثل المتغير أي متغير.

∨ / \ ∧ د / \ ∧ ¬ / \ | أ ∨ ج / \ ج | ب

جميع الصيغ التالية مكتوبة بصيغة النفي العادية:

${\displaystyle {\begin{aligned}&((A\lor B)\land C)\\&(A\lor \lnot B)\\&(A\land \lnot B)\\&((A\land (\lnot B\lor C))\land \lnot C)\end{aligned}}}$

المثال الأول هو أيضًا في الصيغة العادية الاقترانية ، والمثالان التاليان في كل من الصيغة العادية الاقترانية والصيغة العادية الانفصالية ، لكن المثال الأخير ليس في أي منهما.

الصيغ التالية ليست في صيغة النفي العادية:

${\displaystyle {\begin{aligned}(A&\to B)\\\lnot (A&\lor B)\\\lnot (A&\land B)\\\lnot (A&\lor \lnot C)\end{aligned}}}$

إلا أنها تعادل على التوالي الصيغ التالية في شكل النفي الطبيعي:

${\displaystyle {\begin{aligned}(\lnot A&\lor B)\\(\lnot A&\land \lnot B)\\(\lnot A&\lor \lnot B)\\(\lnot A&\land C)\end{aligned}}}$

في المنطق الكلاسيكي والعديد من أنواع المنطق الموجه ، يمكن تحويل أي صيغة إلى هذا الشكل عن طريق استبدال الاستلزام (${\displaystyle \to }$) والمكافئات (${\displaystyle \leftrightarrow }$) وفقًا لتعريفاتهم، باستخدام قوانين دي مورغان لدفع النفي إلى الداخل، وإزالة النفي المزدوج. يمكن تمثيل هذه العملية باستخدام قواعد إعادة الكتابة التالية : ^{[ 1 ]}

${\displaystyle {\begin{aligned}A\to B&~\rightsquigarrow ~\lnot A\lor B\\A\leftrightarrow B&~\rightsquigarrow ~(\lnot A\lor B)\land (A\lor \lnot B)\\\lnot (A\lor B)&~\rightsquigarrow ~\lnot A\land \lnot B\\\lnot (A\land B)&~\rightsquigarrow ~\lnot A\lor \lnot B\\\lnot \lnot A&~\rightsquigarrow ~A\\\lnot \exists xA&~\rightsquigarrow ~\forall x\lnot A\\\lnot \forall xA&~\rightsquigarrow ~\exists x\lnot A\end{aligned}}}$

لا يمكن للتحويل إلى الصيغة العادية المنفية أن يزيد حجم الصيغة إلا بشكل خطي: ​​يظل عدد مرات ظهور الصيغ الذرية كما هو، بينما يظل العدد الإجمالي لمرات ظهور الصيغ الذرية${\displaystyle \land }$و${\displaystyle \lor }$لم يتغير، وعدد مرات حدوث${\displaystyle \lnot }$في الشكل الطبيعي يكون طول الصيغة الأصلية محدودًا.

يمكن تحويل الصيغة في صيغة النفي العادية إلى الصيغة الاقترانية العادية الأقوى أو الصيغة الانفصالية العادية بتطبيق خاصية التوزيع . وقد يؤدي تكرار تطبيق خاصية التوزيع إلى زيادة حجم الصيغة بشكل كبير. في منطق القضايا الكلاسيكي ، لا يؤثر التحويل إلى صيغة النفي العادية على الخصائص الحسابية: إذ تبقى مسألة الإرضاء من فئة NP-كاملة ، وتبقى مسألة الصلاحية من فئة co-NP-كاملة . بالنسبة للصيغ في الصيغة الاقترانية العادية، يمكن حل مسألة الصلاحية في وقت متعدد الحدود، وبالنسبة للصيغ في الصيغة الانفصالية العادية، يمكن حل مسألة الإرضاء في وقت متعدد الحدود.

• الصيغة العادية للوصل
• الصيغة الطبيعية المنفصلة

• روبنسون، جون آلان ؛ فورونكوف، أندريه ، محرران. (2001). دليل الاستدلال الآلي . المجلد  1. مطبعة معهد ماساتشوستس للتكنولوجيا . الصفحات  203 وما بعدها. ISBN 0444829490.

• تطبيق جافا صغير لتحويل الصيغة المنطقية إلى صيغة النفي العادية، مع عرض القوانين المستخدمة.