निषेध सामान्य रूप

गणितीय तर्क में, किसी सूत्र निषेध साधारण रूप (नेगेशन नार्मल फॉर्म, एनएनएफ) में होता है यदि निषेध संक्रियक ($\lnot$, not) केवल चरों पर लागू होता है और केवल द्वितीय अनुमत बूलियन संक्रियक अवश्यक होते हैं जो संयोजन ($\land$, and) और वियोजन ($\lor$, or) हैं।

निषेध सामान्य रूप विहित रूप नहीं है: उदाहरण के लिए, $a\land (b\lor \lnot c)$ और $(a\land b)\lor (a\land \lnot c)$ समतुल्य हैं, और दोनों निषेध सामान्य रूप में हैं।

प्राचीन तर्क और कई मॉडल तर्क में, प्रत्येक सूत्र को उनकी परिभाषाओं द्वारा निहितार्थों और समकक्षों को प्रतिस्थापित करके, निषेध को अंदर की ओर पुश करने के लिए डी मॉर्गन के नियमों का उपयोग करके और दोहरे निषेधों को समाप्त करके इस रूप में लाया जा सकता है। इस प्रक्रिया को निम्नलिखित पुनर्लेखन नियमों का उपयोग करके दर्शाया जा सकता है (स्वचालित तर्क की पुस्तिका 1, पृष्ठ 204):

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

(इन नियमों में, $\Rightarrow$ प्रतीक पुनर्लेखित किए जाने वाले सूत्र में तार्किक निहितार्थ को दर्शाता है, और $\to$ पुनरलेखन ऑपरेशन है।)

निषेध साधारण रूप में परिवर्तन से सूत्र का आकार केवल रैखिक रूप से बढ़ सकता है: परमाणु सूत्रों के घटित होने की संख्या समान रहती है, $\land$ और $\lor$ की कुल परिवर्तन संख्या अभिनिर्मित होती है, और साधारण रूप में $\lnot$ की परिवर्तन संख्या मूल सूत्र की लंबाई से सीमित होती है।

निषेधात्मक साधारण रूप में एक सूत्र को प्रवाल संयोजनिक साधारण रूप या वियोजनिक साधारण रूप में डिस्ट्रीब्यूटिविटी का उपयोग करके डाला जा सकता है। डिस्ट्रीब्यूटिविटी के अनुप्रयोग का बार-बार उपयोग सूत्र का आकार गणनीय रूप से बढ़ा सकता है। चिरसम्मत प्रस्तावीय तर्क में, निषेधात्मक साधारण रूप में परिवर्तन का गणकीय गुण पर प्रभाव नहीं होता है: संतुष्टि समस्या एनपी-पूर्ण ही रहती है, और वैधता समस्या सह-एनपी-पूर्ण ही रहती है। संयोजनिक साधारण रूप में सूत्रों के लिए, वैधता समस्या बहुपद समय में हल की जा सकती है, और वियोजनिक साधारण रूप में सूत्रों के लिए, संतुष्टि समस्या बहुपद समय में हल की जा सकती है।

उदाहरण और प्रति उदाहरण

निम्नलिखित सूत्र सभी निषेधात्मक सामान्य रूप में हैं:

${\begin{aligned}(A&\vee B)\wedge C\\(A&\wedge (\lnot B\vee C)\wedge \lnot C)\vee D\\A&\vee \lnot B\\A&\wedge \lnot B\end{aligned}}$

पहला उदाहरण भी संयोजक सामान्य रूप में है और अंतिम दो उदाहरण संयोजनात्मक सामान्य रूप और वियोजक सामान्य रूप दोनों में हैं, लेकिन दूसरा उदाहरण दोनों में से कोई नहीं है।

निम्नलिखित सूत्र निषेधात्मक सामान्य रूप में नहीं हैं:

${\begin{aligned}A&\Rightarrow B\\\lnot (A&\vee B)\\\lnot (A&\wedge B)\\\lnot (A&\vee \lnot C)\end{aligned}}$

हालाँकि, वे क्रमशः निषेधात्मक सामान्य रूप में निम्नलिखित सूत्रों के समतुल्य हैं:

${\begin{aligned}\lnot A&\vee B\\\lnot A&\wedge \lnot B\\\lnot A&\vee \lnot B\\\lnot A&\wedge C\end{aligned}}$

संदर्भ

• John Alan Robinson and Andrei Voronkov, Handbook of Automated Reasoning 1:203ff (2001) ISBN 0444829490.

बाहरी संबंध

• Java applet for converting logical formula to Negation Normal Form, showing laws used