निषेध सामान्य रूप
गणितीय तर्क में, एक सूत्र नकारात्मक सामान्य रूप (एनएनएफ) में है यदि नकारात्मक ऑपरेटर (, not) केवल चरों पर लागू होता है और केवल अन्य स्वीकृत बूलियन बीजगणित तार्किक संयोजन हैं (, and) और तार्किक संयोजन (, or).
नकारात्मक सामान्य रूप एक विहित रूप नहीं है: उदाहरण के लिए, और समतुल्य हैं, और दोनों नकारात्मक सामान्य रूप में हैं।
विधेय तर्क और कई मॉडल तर्क में, प्रत्येक सूत्र को इस रूप में लाया जा सकता है, उनकी परिभाषाओं द्वारा निहितार्थ और समकक्षों को बदलकर, डी मॉर्गन के कानूनों का उपयोग करके नकारात्मकता को अंदर की ओर धकेला जा सकता है, और दोहरे निषेधों को समाप्त किया जा सकता है। निम्नलिखित पुनर्लेखन नियमों का उपयोग करके इस प्रक्रिया का प्रतिनिधित्व किया जा सकता है (स्वचालित तर्क 1 की पुस्तिका, पृष्ठ 204):
(इन नियमों में, प्रतीक फिर से लिखे जा रहे सूत्र में तार्किक निहितार्थ को इंगित करता है, और पुनर्लेखन ऑपरेशन है।)
अस्वीकरण सामान्य रूप में रूपांतरण केवल एक सूत्र के आकार को रैखिक रूप से बढ़ा सकता है: परमाणु सूत्रों की घटनाओं की संख्या समान रहती है, की घटनाओं की कुल संख्या और अपरिवर्तित है, और की घटनाओं की संख्या सामान्य रूप में मूल सूत्र की लंबाई से घिरा है।
नकारात्मक सामान्य रूप में एक सूत्र को वितरण संपत्ति को लागू करके मजबूत संयोजन सामान्य रूप या वियोगात्मक सामान्य रूप में रखा जा सकता है। वितरण के बार-बार उपयोग से सूत्र के आकार में तेजी से वृद्धि हो सकती है। शास्त्रीय प्रस्तावपरक तर्क में, नकारात्मक सामान्य रूप में परिवर्तन कम्प्यूटेशनल गुणों को प्रभावित नहीं करता है: बूलियन संतुष्टि समस्या एनपी-पूर्ण बनी रहती है, और वैधता समस्या सह-एनपी-पूर्ण बनी रहती है। संयोजक सामान्य रूप में सूत्रों के लिए, वैधता समस्या बहुपद समय में हल करने योग्य है, और वियोगी सामान्य रूप में सूत्रों के लिए, बहुपद समय में संतोषजनक समस्या हल करने योग्य है।
उदाहरण और प्रति उदाहरण
निम्नलिखित सूत्र सभी नकारात्मक सामान्य रूप में हैं:
पहला उदाहरण संयोजन सामान्य रूप में भी है और अंतिम दो संयोजन सामान्य रूप और वियोगी सामान्य रूप दोनों में हैं, लेकिन दूसरा उदाहरण न तो है।
निम्नलिखित सूत्र नकारात्मक सामान्य रूप में नहीं हैं:
हालाँकि, वे क्रमशः नकारात्मक सामान्य रूप में निम्नलिखित सूत्रों के बराबर हैं:
संदर्भ
- John Alan Robinson and Andrei Voronkov, Handbook of Automated Reasoning 1:203ff (2001) ISBN 0444829490.