संयोजक सामान्य रूप

Not to be confused with चॉम्स्की सामान्य रूप.

बूलियन तर्क में, एक सूत्र (गणितीय तर्क) संयोजक सामान्य रूप (सीएनएफ) या खंड सामान्य रूप में होता है यदि यह एक या अधिक खंडो(तर्क) का तार्किक संयोजन है, जहां एक खंड शाब्दिक (गणितीय तर्क) का विच्छेदन है; अन्यथा कहें तो, यह योगों या ओआरएस के एंड का उत्पाद है। एक विहित सामान्य रूप के रूप में, यह स्वचालित प्रमेय सिद्ध करने और सर्किट सिद्धांत में उपयोगी है।

शाब्दिकों के सभी संयोजन और शाब्दिकों के सभी विच्छेदन सीएनएफ में हैं, क्योंकि उन्हें क्रमशः एक-शाब्दिक खंड के संयोजन और एक एकल खंड के संयोजन के रूप में देखा जा सकता है। जैसा कि विच्छेदात्मक सामान्य रूप (डीएनएफ) में होता है, सीएनएफ में एक सूत्र में सम्मलित होने वाले एकमात्र प्रस्तावक संयोजक तार्किक संयोजन, तार्किक वियोजन और तार्किक निषेध हैं। नॉट ऑपरेटर का उपयोग केवल शाब्दिक भाग के रूप में किया जा सकता है, जिसका अर्थ है कि यह केवल एक प्रस्तावात्मक चर या एक विधेय प्रतीक से पहले हो सकता है।

स्वचालित प्रमेय सिद्ध करने में, धारणा "खंड सामान्य रूप" का उपयोग अधिकांशतः एक संकीर्ण अर्थ में किया जाता है, जिसका अर्थ शाब्दिक समुच्चय के समुच्चय के रूप में सीएनएफ सूत्र का एक विशेष प्रतिनिधित्व होता है।

उदाहरण और गैर-उदाहरण

निम्नलिखित सभी सूत्र चर में हैं $A,B,C,D,E$, और $F$ संयोजक सामान्य रूप में हैं:

• $(A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F)$
• $(A\lor B)\land (C)$
• $(A\lor B)$
• $(A)$

स्पष्टता के लिए, विभक्ति खंड ऊपर कोष्ठक के अंदर लिखे गए हैं। कोष्ठक में रखे गए संयोजक खंडो के साथ विच्छेदात्मक सामान्य रूप में, अंतिम स्थिति वही है, लेकिन अंतिम से अगला है $(A)\lor (B)$. स्थिरांक सत्य और असत्य को खाली संयुक्ताक्षर और खाली विच्छेद से युक्त एक खंड द्वारा दर्शाया जाता है, लेकिन सामान्यतः स्पष्ट रूप से लिखा जाता है।

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

• $\neg (B\lor C)$, क्योंकि ओआर एक नॉट के भीतर निहित है
• $(A\land B)\lor C$
• $A\land (B\lor (D\land E))$, चूँकि एंड एक ओआर के भीतर निहित है

प्रत्येक सूत्र को संयोजक सामान्य रूप में एक सूत्र के रूप में समान रूप से लिखा जा सकता है। सीएनएफ में तीन गैर-उदाहरण हैं:

• $(\neg B)\land (\neg C)$
• $(A\lor C)\land (B\lor C)$
• $(A)\land (B\lor D)\land (B\lor E).$

सीएनएफ में रूपांतरण

प्रत्येक प्रस्तावात्मक सूत्र को सीएनएफ में उपस्थित तार्किक तुल्यता सूत्र में परिवर्तित किया जा सकता है। यह परिवर्तन तार्किक तुल्यता के नियमों पर आधारित है: दोहरा निषेध उन्मूलन, डी मॉर्गन के नियम और वितरणात्मक नियम।

चूंकि सभी प्रस्तावक सूत्रों को संयोजक सामान्य रूप में समकक्ष सूत्र में परिवर्तित किया जा सकता है, इसलिए प्रमाण अधिकांशतः इस धारणा पर आधारित होते हैं कि सभी सूत्र सीएनएफ हैं। चूंकि, कुछ स्थितियों में सीएनएफ में यह रूपांतरण सूत्र के तेजी से विस्फोट का कारण बन सकता है। उदाहरण के लिए, निम्नलिखित गैर-सीएनएफ सूत्र को सीएनएफ में अनुवाद करने से एक सूत्र तैयार होता है $2^{n}$ खंड:

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

विशेष रूप से, उत्पन्न सूत्र है:

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

इस सूत्र में सम्मलित है $2^{n}$ खंड; प्रत्येक खंड में या तो सम्मलित है $X_{i}$ या $Y_{i}$ प्रत्येक के लिए $i$.

सीएनएफ में ऐसे परिवर्तन उपस्थित हैं जो तार्किक तुल्यता के अतिरिक्त बूलियन संतुष्टि समस्या को संरक्षित करके आकार में तेजी से वृद्धि से बचते हैं। ये परिवर्तन केवल सूत्र के आकार को रैखिक रूप से बढ़ाने की गारंटी देते हैं, लेकिन नए चर पेश करते हैं। उदाहरण के लिए, उपरोक्त सूत्र को चर जोड़कर सीएनएफ में बदला जा सकता है $Z_{1},\ldots ,Z_{n}$ इस प्रकार है:

$(Z_{1}\vee \cdots \vee Z_{n})\wedge (\neg Z_{1}\vee X_{1})\wedge (\neg Z_{1}\vee Y_{1})\wedge \cdots \wedge (\neg Z_{n}\vee X_{n})\wedge (\neg Z_{n}\vee Y_{n}).$

एक व्याख्या (तर्क) इस सूत्र को तभी संतुष्ट करती है जब कम से कम एक नया चर सत्य हो। यदि यह चर है $Z_{i}$, फिर दोनों $X_{i}$ और $Y_{i}$ भी सत्य हैं। इसका तात्पर्य यह है कि प्रत्येक मॉडल सिद्धांत जो इस सूत्र को संतुष्ट करता है वह मूल सिद्धांत को भी संतुष्ट करता है। दूसरी ओर, मूल सूत्र के केवल कुछ मॉडल ही इसे संतुष्ट करते हैं: मूल सूत्र में $Z_{i}$ का उल्लेख नहीं किया गया है, उनके मान इसकी संतुष्टि के लिए अप्रासंगिक हैं, जो कि अंतिम सूत्र में नहीं है। इसका तात्पर्य यह है कि मूल सूत्र और अनुवाद का परिणाम समान (गणितीय तर्क) है लेकिन तार्किक समतुल्य नहीं है।

एक वैकल्पिक अनुवाद, त्सेइटिन परिवर्तन में खंड भी सम्मलित हैं $Z_{i}\vee \neg X_{i}\vee \neg Y_{i}$. इन खंडो से सूत्र का तात्पर्य है $Z_{i}\equiv X_{i}\wedge Y_{i}$; इस सूत्र को अधिकांशतः "परिभाषित" माना जाता है $Z_{i}$ के लिए एक नाम होना $X_{i}\wedge Y_{i}$.

प्रथम-क्रम तर्क

प्रथम क्रम तर्क में, तार्किक सूत्र के खंड सामान्य रूप को प्राप्त करने के लिए संयोजक सामान्य रूप को आगे ले जाया जा सकता है, जिसका उपयोग प्रथम-क्रम समाधान करने के लिए किया जा सकता है। रिज़ॉल्यूशन-आधारित स्वचालित प्रमेय-सिद्ध करने में, एक सीएनएफ सूत्र

$($

$l_{11}$

$\lor$

$\ldots$

$\lor$

$l_{1n_{1}}$

$)$

$\land$

$\ldots$

$\land$

$($

$l_{m1}$

$\lor$

$\ldots$

$\lor$

$l_{mn_{m}}$

$)$

, साथ $l_{ij}$ शाब्दिक, सामान्यतः समुच्चय के एक समुच्चय के रूप में दर्शाया जाता है

$\{$

$\{$

$l_{11}$

$,$

$\ldots$

$,$

$l_{1n_{1}}$

$\}$

$,$

$\ldots$

$,$

$\{$

$l_{m1}$

$,$

$\ldots$

$,$

$l_{mn_{m}}$

$\}$

$\}$

.

कम्प्यूटेशनल जटिलता

कम्प्यूटेशनल जटिलता सिद्धांत में समस्याओं के एक महत्वपूर्ण समुच्चय में संयोजक सामान्य रूप में व्यक्त बूलियन सूत्र के चर के लिए असाइनमेंट ढूंढना सम्मलित है, जैसे कि सूत्र सत्य है। K-समुच्चय समस्या सीएनएफ में व्यक्त बूलियन सूत्र के लिए एक संतोषजनक असाइनमेंट जाँचने की समस्या है जिसमें प्रत्येक वियोजन में अधिकतम k चर होते हैं। 3-समुच्चय एनपी-पूर्ण है (k>2 के साथ किसी भी अन्य k-समुच्चय समस्या की तरह) जबकि 2-संतोषजनकता, 2-समुच्चय को बहुपद समय में समाधान के लिए जाना जाता है। परिणामस्वरूप, किसी सूत्र को डीएनएफ में परिवर्तित करने, संतुष्टि बनाए रखने का कार्य एनपी कठिन है; दोहरी रूप से, सीएनएफ में परिवर्तित करना, वैधता को संरक्षित करना भी एनपी-हार्ड है; इसलिए डीएनएफ या सीएनएफ में समतुल्य-संरक्षण रूपांतरण फिर से एनपी-हार्ड है।

इस मामले में विशिष्ट समस्याओं में "3सीएनएफ" में सूत्र सम्मलित हैं: संयोजक सामान्य रूप जिसमें प्रति संयोजन तीन से अधिक चर न हों। व्यवहार में आने वाले ऐसे सूत्रों के उदाहरण बहुत बड़े हो सकते हैं, उदाहरण के लिए 100,000 चर और 1,000,000 संयोजन के साथ।

सीएनएफ में एक सूत्र को प्रत्येक संयोजन को k से अधिक चर के साथ प्रतिस्थापित करके "केसीएनएफ" (k≥3 के लिए) में एक समतुल्य सूत्र में परिवर्तित किया जा सकता है। $X_{1}\vee \cdots \vee X_{k}\vee \cdots \vee X_{n}$ दो संयोजकों द्वारा $X_{1}\vee \cdots \vee X_{k-1}\vee Z$ और $\neg Z\vee X_{k}\cdots \vee X_{n}$ , Z के साथ एक नया चर, और जितनी बार आवश्यक हो दोहराना।

प्रथम-क्रम तर्क से परिवर्तित करना

प्रथम-क्रम तर्क को सीएनएफ में परिवर्तित करने के लिए:

1. निषेध को सामान्य रूप में परिवर्तित करें
   1. निहितार्थ और तुल्यताएँ हटाएँ: बार-बार परिवर्तित करें $P\rightarrow Q$ साथ $\lnot P\lor Q$; बदलना $P\leftrightarrow Q$ साथ $(P\lor \lnot Q)\land (\lnot P\lor Q)$. अंततः, यह की सभी घटनाओं को समाप्त कर देगा $\rightarrow$ और $\leftrightarrow$.
   2. डी मॉर्गन के नियम को बार-बार क्रियान्वित करके नोट को अंदर की ओर ले जाएं। विशेष रूप से, प्रतिस्थापित करें $\lnot (P\lor Q)$ साथ $(\lnot P)\land (\lnot Q)$; बदलना $\lnot (P\land Q)$ साथ $(\lnot P)\lor (\lnot Q)$; और बदलें $\lnot \lnot P$ साथ $P$; बदलना $\lnot (\forall xP(x))$ साथ $\exists x\lnot P(x)$; $\lnot (\exists xP(x))$ साथ $\forall x\lnot P(x)$. उसके पश्चात, ए $\lnot$ विधेय चिह्न के ठीक पहले ही घटित हो सकता है।
2. चरों का मानकीकरण करें
   1. जैसे वाक्यों के लिए $(\forall xP(x))\lor (\exists xQ(x))$ जो एक ही चर नाम का दो बार उपयोग करते हैं, उनमें से एक चर का नाम बदल देते हैं।इससे पश्चात में क्वांटिफायर छोड़ते समय भ्रम की स्थिति से बचा जा सकता है। उदाहरण के लिए, $\forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists y\mathrm {Loves} (y,x)]$ का नाम बदल दिया गया है $\forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists z\mathrm {Loves} (z,x)]$.
3. स्टेटमेन को स्कोलेम सामान्य रूप करें
   1. क्वांटिफायर को बाहर की ओर ले जाएं: बार-बार बदलें $P\land (\forall xQ(x))$ साथ $\forall x(P\land Q(x))$; बदलना $P\lor (\forall xQ(x))$ साथ $\forall x(P\lor Q(x))$; बदलना $P\land (\exists xQ(x))$ साथ $\exists x(P\land Q(x))$; बदलना $P\lor (\exists xQ(x))$ साथ $\exists x(P\lor Q(x))$. ये प्रतिस्थापन समतुल्यता को संरक्षित करते हैं, क्योंकि पिछले परिवर्तनीय मानकीकरण चरण ने यह सुनिश्चित किया था जहां $x$ में नहीं होता है $P$. इन प्रतिस्थापनों के पश्चात, एक क्वांटिफ़ायर केवल सूत्र के प्रारंभिक उपसर्ग में हो सकता है, लेकिन कभी भी a के अंदर नहीं $\lnot$, $\land$, या $\lor$.
   2. बार-बार बदलें $\forall x_{1}\ldots \forall x_{n}\;\exists y\;P(y)$ साथ $\forall x_{1}\ldots \forall x_{n}\;P(f(x_{1},\ldots ,x_{n}))$, जहां $f$ एक नया है $n$-एरी फलन प्रतीक, एक तथाकथित "स्कोलेम फलन"। यह एकमात्र कदम है जो समतुल्यता के अतिरिक्त केवल संतुष्टि को निरंतर रखता है। यह सभी अस्तित्व संबंधी परिमाणकों को समाप्त कर देता है।
4. सभी सार्वभौमिक परिमाणकों को छोड़ें।
5. ओआरएस को एंड के ऊपर अंदर की ओर वितरित करें: बार-बार बदलें $P\lor (Q\land R)$ साथ $(P\lor Q)\land (P\lor R)$.

उदाहरण के तौर पर, सूत्र कहता है कि "जो कोई भी सभी जानवरों से प्यार करता है, वह बदले में किसी से प्यार करता है" को सीएनएफ में परिवर्तित किया जाता है (और पश्चात में अंतिम पंक्ति में खंड फॉर्म में) निम्नानुसार (प्रतिस्थापन नियम रिडेक्स को हाइलाइट करना) ${\color {red}{\text{red}}}$):

$\forall x$

$($

$\forall y$

$\mathrm {Animal} ($

$y$

$)$

$\color {red}\rightarrow$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\rightarrow$

$($

$\exists$

$y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

$\forall x$

$($

$\forall y$

$\lnot$

$\mathrm {Animal} ($

$y$

$)$

$\lor$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\color {red}\rightarrow$

$($

$\exists$

$y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

by 1.1

$\forall x$

$\color {red}\lnot$

$($

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

$\lnot$

$\mathrm {Animal} ($

$y$

$)$

$\lor$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\lor$

$($

$\exists$

$y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

by 1.1

$\forall x$

$($

$\exists y$

$\color {red}\lnot$

$($

$\lnot$

$\mathrm {Animal} ($

$y$

$)$

$\color {red}\lor$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$)$

$\lor$

$($

$\exists$

$y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

by 1.2

$\forall x$

$($

$\exists y$

$\color {red}\lnot$

$\color {red}\lnot$

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\lor$

$($

$\exists$

$y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

by 1.2

$\forall x$

$($

${\color {red}{\exists y}}$

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\lor$

$($

$\color {red}\exists$

$\color {red}y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

by 1.2

$\forall x$

$($

$\exists y$

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\color {red}\lor$

$($

$\color {red}\exists$

$\color {red}z$

$\mathrm {Loves} ($

$z$

$,x)$

$)$

by 2

$\forall x$

$\exists z$

$($

${\color {red}{\exists y}}$

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\color {red}\lor$

$\mathrm {Loves} ($

$z$

$,x)$

by 3.1

$\forall x$

${\color {red}{\exists z}}$

$\exists y$

$($

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\lor$

$\mathrm {Loves} ($

$z$

$,x)$

by 3.1

$\forall x$

${\color {red}{\exists y}}$

$($

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\lor$

$\mathrm {Loves} ($

$g(x)$

$,x)$

by 3.2

$($

$\mathrm {Animal} ($

$f(x)$

$)$

$\color {red}\land$

$\lnot$

$\mathrm {Loves} (x,$

$f(x)$

$)$

$)$

$\color {red}\lor$

$\mathrm {Loves} ($

$g(x)$

$,x)$

by 4

$($

$\mathrm {Animal} ($

$f(x)$

$)$

$\color {red}\lor$

$\mathrm {Loves} ($

$g(x)$

$,x)$

$)$

$\color {red}\land$

$($

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

$\color {red}\lor$

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

$)$

by 5

$\{$

$\{$

$\mathrm {Animal} ($

$f(x)$

$)$

$,$

$\mathrm {Loves} ($

$g(x)$

$,x)$

$\}$

$,$

$\{$

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

$,$

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

$\}$

$\}$

(clause representation)

अनौपचारिक रूप से, स्कोलेम फलन $g(x)$ को उस व्यक्ति की उपज के रूप में सोचा जा सकता है जिसके द्वारा $x$ को लव्ड किया जाता है, जबकि $f(x)$ से एनिमल (यदि कोई हो) प्राप्त होता है $x$ लव्ड नहीं करता. नीचे से तीसरी अंतिम पंक्ति इस प्रकार है " $x$ को एनिमल से लव्ड नहीं है $f(x)$, या फिर $x$ से लव्ड है $g(x)$.

ऊपर से दूसरी अंतिम पंक्ति, $(\mathrm {Animal} (f(x))\lor \mathrm {Loves} (g(x),x))\land (\lnot \mathrm {Loves} (x,f(x))\lor \mathrm {Loves} (g(x),x))$, सीएनएफ है।

यह भी देखें

• बीजगणितीय सामान्य रूप
• विच्छेदनात्मक सामान्य रूप
• हॉर्न खंड
• क्वीन-मैक्लुस्की एल्गोरिथम

संदर्भ

• जे एल्डन व्हाइटसिट (24 मई 2012). बूलियन बीजगणित और इसके अनुप्रयोग. कूरियर निगम. ISBN 978-0-486-15816-7. {{cite book}}: Check date values in: |date= (help)
• हंस क्लेन बुनिंग; थियोडोर लेटमैन (28 अगस्त 1999). प्रस्तावात्मक तर्क: कटौती और एल्गोरिदम. कैम्ब्रिज यूनिवर्सिटी प्रेस. ISBN 978-0-521-63017-7. {{cite book}}: Check date values in: |date= (help)
• पॉल जैक्सन, डैनियल शेरिडन: बूलियन सर्किट के लिए खंड फॉर्म रूपांतरण।. में: होल्गर एच. हूस, डेविड जी. मिशेल (सं.): संतुष्टि परीक्षण के सिद्धांत और अनुप्रयोग, 7वां अंतर्राष्ट्रीय सम्मेलन, एसएटी 2004, वैंकूवर, बीसी, कनाडा, 10-13 मई, 2004, संशोधित चयनित पेपर। कंप्यूटर विज्ञान में व्याख्यान नोट्स 3542, स्प्रिंगर 2005, पीपी 183-198
• जी.एस. त्सेतिन: प्रस्तावात्मक कलन में व्युत्पत्ति की जटिलता पर. में: स्लिसेंको, ए.ओ. (ईडी।) रचनात्मक गणित और गणितीय तर्क में संरचनाएं, भाग II, गणित में सेमिनार (रूसी से अनुवादित), पीपी 115-125। स्टेक्लोव गणितीय संस्थान (1968)

बाहरी संबंध

• "संयोजक सामान्य रूप", Encyclopedia of Mathematics, EMS Press, 2001 [1994]
• सत्य तालिका को सीएनएफ और डीएनएफ में परिवर्तित करने के लिए जावा टूल
• जावा टूल के लिए सीएनएफ और डीएनएफ में बदलाव किया गया