प्रूफ कॉम्पलेक्सिटी: Difference between revisions

From Vigyanwiki
No edit summary
No edit summary
Line 1: Line 1:
[[तर्क]] और [[सैद्धांतिक कंप्यूटर विज्ञान]] में, और विशेष रूप से [[प्रमाण सिद्धांत]] और [[कम्प्यूटेशनल जटिलता सिद्धांत|कम्प्यूटेशनल कॉम्पलेक्सिटी सिद्धांत]] में, प्रूफ कॉम्पलेक्सिटी वह क्षेत्र है जिसका लक्ष्य उन कम्प्यूटेशनल संसाधनों का अध्ययन और उनका विश्लेषण करना है जो स्टेटमेंट्स को सिद्ध करने अथवा खंडन करने के लिए आवश्यक हैं। प्रूफ कॉम्पलेक्सिटी में अनुसंधान मुख्य रूप से विभिन्न प्रस्ताव प्रमाण प्रणालियों में प्रमाण-लंबाई की निचली और ऊपरी सीमा को सिद्ध करने से संबंधित है। उदाहरण के लिए, प्रूफ कॉम्पलेक्सिटी के प्रमुख प्रवादों में से यह दर्शाना है कि फ़्रीज सिस्टम, सामान्य [[प्रस्तावात्मक कलन]], सभी टॉटोलॉजीज़ के बहुपद-आकार के प्रमाणों को स्वीकार नहीं करता है। यहां प्रमाण का आकार केवल उसमें प्रतीकों की संख्या है, और प्रमाण को बहुपद आकार का कहा जाता है यदि यह टॉटोलॉजी के आकार में बहुपद है जो इसे सिद्ध करता है।
[[तर्क|लॉजिक]] और [[सैद्धांतिक कंप्यूटर विज्ञान]] में, और विशेष रूप से [[प्रमाण सिद्धांत]] और [[कम्प्यूटेशनल जटिलता सिद्धांत|कम्प्यूटेशनल कॉम्पलेक्सिटी सिद्धांत]] में, प्रूफ कॉम्पलेक्सिटी वह क्षेत्र है जिसका लक्ष्य उन कम्प्यूटेशनल संसाधनों का अध्ययन और उनका विश्लेषण करना है जो स्टेटमेंट्स को सिद्ध करने अथवा खंडन करने के लिए आवश्यक हैं। प्रूफ कॉम्पलेक्सिटी में अनुसंधान मुख्य रूप से विभिन्न प्रस्ताव प्रमाण प्रणालियों में प्रमाण-लंबाई की निचली और ऊपरी सीमा को सिद्ध करने से संबंधित है। उदाहरण के लिए, प्रूफ कॉम्पलेक्सिटी के प्रमुख प्रवादों में से यह दर्शाना है कि फ़्रीज सिस्टम, सामान्य [[प्रस्तावात्मक कलन]], सभी टॉटोलॉजीज़ के बहुपद-आकार के प्रमाणों को स्वीकार नहीं करता है। यहां प्रमाण का आकार केवल उसमें प्रतीकों की संख्या है, और प्रमाण को बहुपद आकार का कहा जाता है यदि यह टॉटोलॉजी के आकार में बहुपद है जो इसे सिद्ध करता है।


प्रूफ कॉम्पलेक्सिटी का व्यवस्थित अध्ययन [[स्टीफन कुक]] और [[रॉबर्ट रेकहो]] (1979) के कार्य से प्रारम्भ हुआ, जिन्होंने कम्प्यूटेशनल कॉम्पलेक्सिटी के परिप्रेक्ष्य से [[प्रस्ताव प्रमाण प्रणाली]] की मूल परिभाषा प्रदान की थी। विशेष रूप से कुक और रेकहो ने देखा कि दृढ़ प्रोपोज़िशनल [[फ्रीज प्रणाली|प्रूफ़ सिस्टम]] पर प्रूफ साइज की निचली सीमा सिद्ध करने को [[पी (जटिलता)|NP (कॉम्पलेक्सिटी)]] को coNP से पृथक करने की दिशा में चरण के रूप में देखा जा सकता है (और इस प्रकार NP से P (कॉम्पलेक्सिटी)), क्योंकि प्रोपोज़िशनल प्रूफ़ सिस्टम का अस्तित्व है जो बहुपद आकार के प्रमाणों को स्वीकार करता है, सभी टॉटोलॉजी के लिए NP=coNP के समान है।
प्रूफ कॉम्पलेक्सिटी का व्यवस्थित अध्ययन [[स्टीफन कुक]] और [[रॉबर्ट रेकहो]] (1979) के कार्य से प्रारम्भ हुआ, जिन्होंने कम्प्यूटेशनल कॉम्पलेक्सिटी के परिप्रेक्ष्य से [[प्रस्ताव प्रमाण प्रणाली]] की मूल परिभाषा प्रदान की थी। विशेष रूप से कुक और रेकहो ने देखा कि दृढ़ प्रोपोज़िशनल [[फ्रीज प्रणाली|प्रूफ़ सिस्टम]] पर प्रूफ साइज की निचली सीमा सिद्ध करने को [[पी (जटिलता)|NP (कॉम्पलेक्सिटी)]] को coNP से पृथक करने की दिशा में चरण के रूप में देखा जा सकता है (और इस प्रकार NP से P (कॉम्पलेक्सिटी)), क्योंकि प्रोपोज़िशनल प्रूफ़ सिस्टम का अस्तित्व है जो बहुपद आकार के प्रमाणों को स्वीकार करता है, सभी टॉटोलॉजी के लिए NP=coNP के समान है।
Line 5: Line 5:
समसामयिक प्रूफ कॉम्पलेक्सिटी अनुसंधान कम्प्यूटेशनल कॉम्पलेक्सिटी, [[कलन विधि]] और गणित के कई क्षेत्रों से विचार और विधियाँ प्राप्त करता है। यद्यपि कई महत्वपूर्ण एल्गोरिदम और एल्गोरिदमिक तकनीकों को कुछ प्रूफ सिस्टमों के लिए प्रूफ सर्च एल्गोरिदम के रूप में निक्षेप किया जा सकता है, इसलिए इन सिस्टमों में प्रूफ आकारों पर निचली सीमाएं सिद्ध करते हैं, इसका अर्थ है कि संबंधित एल्गोरिदम पर रन-टाइम निचली सीमाएं होती हैं। यह प्रूफ कॉम्पलेक्सिटी को SAT सॉल्वर जैसे अधिक व्यावहारिक क्षेत्रों से संयोजित करता है।
समसामयिक प्रूफ कॉम्पलेक्सिटी अनुसंधान कम्प्यूटेशनल कॉम्पलेक्सिटी, [[कलन विधि]] और गणित के कई क्षेत्रों से विचार और विधियाँ प्राप्त करता है। यद्यपि कई महत्वपूर्ण एल्गोरिदम और एल्गोरिदमिक तकनीकों को कुछ प्रूफ सिस्टमों के लिए प्रूफ सर्च एल्गोरिदम के रूप में निक्षेप किया जा सकता है, इसलिए इन सिस्टमों में प्रूफ आकारों पर निचली सीमाएं सिद्ध करते हैं, इसका अर्थ है कि संबंधित एल्गोरिदम पर रन-टाइम निचली सीमाएं होती हैं। यह प्रूफ कॉम्पलेक्सिटी को SAT सॉल्वर जैसे अधिक व्यावहारिक क्षेत्रों से संयोजित करता है।


[[गणितीय तर्क]] प्रस्तावित प्रमाण आकारों का अध्ययन करने के लिए फ्रेमवर्क के रूप में भी कार्य कर सकता है। [[प्रथम-क्रम सिद्धांत]] और, विशेष रूप से, [[पीनो अंकगणित]] के वीक फ्रेगमेंट, जो सीमित अंकगणित के नाम से आते हैं, प्रस्ताव प्रमाण प्रणालियों के समान संस्करणों के रूप में कार्य करते हैं और व्यवहार्य तर्क के विभिन्न स्तरों के संदर्भ में लघु प्रस्ताव प्रमाणों की व्याख्या के लिए अग्र पृष्ठभूमि प्रदान करते हैं।
[[गणितीय तर्क|गणितीय लॉजिक]] प्रस्तावित प्रमाण आकारों का अध्ययन करने के लिए फ्रेमवर्क के रूप में भी कार्य कर सकता है। [[प्रथम-क्रम सिद्धांत]] और, विशेष रूप से, [[पीनो अंकगणित]] के वीक फ्रेगमेंट, जो सीमित अंकगणित के नाम से आते हैं, प्रस्ताव प्रमाण प्रणालियों के समान संस्करणों के रूप में कार्य करते हैं और व्यवहार्य लॉजिक के विभिन्न स्तरों के संदर्भ में लघु प्रस्ताव प्रमाणों की व्याख्या के लिए अग्र पृष्ठभूमि प्रदान करते हैं।


==प्रमाण प्रणालियाँ==
==प्रमाण प्रणालियाँ==
{{Main|प्रस्ताव प्रमाण प्रणाली}}
{{Main|प्रोपोज़िशनल प्रूफ सिस्टम}}


प्रस्तावक प्रमाण प्रणाली को दो इनपुट के साथ प्रमाण-सत्यापन एल्गोरिथ्म P(A,x) के रूप में दिया गया है। यदि P पेयर (A,x) को स्वीकार करता है तो हम कहते हैं कि x, A का P-प्रूफ है। P को बहुपद समय में रन करना आवश्यक है, और इसके अतिरिक्त यह मानना ​​होगा कि A के निकट P-प्रूफ है यदि A टॉटोलॉजी है।
प्रोपोज़िशनल प्रूफ सिस्टम को दो इनपुट के साथ प्रमाण-सत्यापन एल्गोरिथ्म P(A,x) के रूप में दिया गया है। यदि P पेयर (A,x) को स्वीकार करता है तो हम कहते हैं कि x, A का P-प्रूफ है। P को बहुपद समय में रन करना आवश्यक है, और इसके अतिरिक्त यह मानना ​​होगा कि A के निकट P-प्रूफ है यदि A टॉटोलॉजी है।


प्रस्तावक प्रमाण प्रणाली के उदाहरणों में अनुक्रमिक कलन, रिज़ॉल्यूशन (तर्क), [[कटिंग-प्लेन विधि]] और फ़्रीज सिस्टम सम्मिलित हैं। [[ज़र्मेलो फ्रेंकेल सेट सिद्धांत]] जैसे दृढ़ गणितीय सिद्धांत प्रस्तावात्मक प्रमाण प्रणालियों को भी प्रेरित करते हैं: ZFC की प्रस्तावात्मक व्याख्या में टॉटोलॉजी <math>\tau</math> का प्रमाण औपचारिक कथन '<math>\tau</math> टॉटोलॉजी है' का ZFC-प्रमाण है।
प्रोपोज़िशनल प्रूफ सिस्टम के उदाहरणों में अनुक्रमिक कलन, रिज़ॉल्यूशन (लॉजिक), [[कटिंग-प्लेन विधि]] और फ़्रीज सिस्टम सम्मिलित हैं। [[ज़र्मेलो फ्रेंकेल सेट सिद्धांत]] जैसे दृढ़ गणितीय सिद्धांत प्रस्तावात्मक प्रमाण प्रणालियों को भी प्रेरित करते हैं: ZFC की प्रस्तावात्मक व्याख्या में टॉटोलॉजी <math>\tau</math> का प्रमाण औपचारिक कथन '<math>\tau</math> टॉटोलॉजी है' का ZFC-प्रमाण है।


==बहुपद आकार के प्रमाण और NP के प्रति coNP समस्या==
==बहुपद आकार के प्रमाण और NP के प्रति coNP समस्या==
Line 65: Line 65:
{{Main|परिबद्ध अंकगणित}}
{{Main|परिबद्ध अंकगणित}}


प्रस्तावित प्रमाण प्रणालियों की व्याख्या उच्च क्रम के सिद्धांतों के असमान समकक्षों के रूप में की जा सकती है। समतुल्यता का अध्ययन अधिकांशतः परिबद्ध अंकगणित के सिद्धांतों के संदर्भ में किया जाता है। उदाहरण के लिए, विस्तारित फ़्रीज प्रणाली कुक के सिद्धांत <math>\mathrm {PV}_1</math> से युग्मित होती है जो बहुपद-समय तर्क को औपचारिक बनाती है और फ़्रीज प्रणाली <math>\mathsf{NC}^1</math> तर्क को औपचारिक बनाने वाले सिद्धांत <math>\mathrm {VNC}^1</math> से युग्मित होती है।
प्रस्तावित प्रमाण प्रणालियों की व्याख्या उच्च क्रम के सिद्धांतों के असमान समकक्षों के रूप में की जा सकती है। समतुल्यता का अध्ययन अधिकांशतः परिबद्ध अंकगणित के सिद्धांतों के संदर्भ में किया जाता है। उदाहरण के लिए, विस्तारित फ़्रीज प्रणाली कुक के सिद्धांत <math>\mathrm {PV}_1</math> से युग्मित होती है जो बहुपद-समय लॉजिक को औपचारिक बनाती है और फ़्रीज प्रणाली <math>\mathsf{NC}^1</math> लॉजिक को औपचारिक बनाने वाले सिद्धांत <math>\mathrm {VNC}^1</math> से युग्मित होती है।


पत्राचार स्टीफन कुक (1975) द्वारा प्रस्तुत किया गया था, जिन्होंने दिखाया <math>\mathrm {PV}_1</math> के सीओएनपी प्रमेय, औपचारिक रूप से <math>\Pi^b_1</math> सूत्र, विस्तारित फ़्रीज में बहुपद-आकार के प्रमाणों के साथ टॉटोलॉजी के अनुक्रम में अनुवाद करते हैं। इसके अतिरिक्त, एक्सटेंडेड फ्रीज इस प्रकार की सबसे अशक्त प्रणाली है: यदि किसी अन्य प्रूफ सिस्टम P में यह गुण है, तो P एक्सटेंडेड फ्रीज का अनुकरण करता है।<ref name="cook">{{cite book|first1=Stephen|last1=Cook|author-link1=Stephen Cook|chapter=Feasibly constructive proofs and the propositiona calculus|title=Proceedings of the 7th Annual ACM Symposium on Theory of Computing|year=1975|pages=83–97}}</ref>
पत्राचार स्टीफन कुक (1975) द्वारा प्रस्तुत किया गया था, जिन्होंने दिखाया <math>\mathrm {PV}_1</math> के सीओएनपी प्रमेय, औपचारिक रूप से <math>\Pi^b_1</math> सूत्र, विस्तारित फ़्रीज में बहुपद-आकार के प्रमाणों के साथ टॉटोलॉजी के अनुक्रम में अनुवाद करते हैं। इसके अतिरिक्त, एक्सटेंडेड फ्रीज इस प्रकार की सबसे अशक्त प्रणाली है: यदि किसी अन्य प्रूफ सिस्टम P में यह गुण है, तो P एक्सटेंडेड फ्रीज का अनुकरण करता है।<ref name="cook">{{cite book|first1=Stephen|last1=Cook|author-link1=Stephen Cook|chapter=Feasibly constructive proofs and the propositiona calculus|title=Proceedings of the 7th Annual ACM Symposium on Theory of Computing|year=1975|pages=83–97}}</ref>
Line 79: Line 79:
  | year = 2010}} ([http://www.cs.toronto.edu/~sacook/homepage/book draft from 2008])</ref>
  | year = 2010}} ([http://www.cs.toronto.edu/~sacook/homepage/book draft from 2008])</ref>


जबकि उपर्युक्त पत्राचार कहता है कि सिद्धांत में प्रमाण संबंधित प्रमाण प्रणाली में लघु प्रमाणों के अनुक्रम में परिवर्तन हो जाता है, तथा विपरीत निहितार्थ का रूप भी प्रस्तावित होता है। सिस्टम P के अनुरूप सिद्धांत T के उपयुक्त [[मॉडल (तर्क)]] का निर्माण करके प्रमाण प्रणाली P में प्रमाण के आकार पर निचली सीमा प्राप्त करना संभव है। यह [[मॉडल-सैद्धांतिक]] निर्माणों के माध्यम से कॉम्पलेक्सिटी की निचली सीमा को सिद्ध करने की अनुमति देता है, तथा दृष्टिकोण जिसे मिक्लोस अजताई की विधि के रूप में जाना जाता है।<ref name="Ajt">{{cite book|first1=M.|last1=Ajtai|author-link1=Miklós Ajtai|chapter=The complexity of the pigeonhole principle|title=Proceedings of the IEEE 29th Annual Symposium on Foundation of Computer Science|year=1988|pages=346–355}}</ref>
जबकि उपर्युक्त पत्राचार कहता है कि सिद्धांत में प्रमाण संबंधित प्रमाण प्रणाली में लघु प्रमाणों के अनुक्रम में परिवर्तन हो जाता है, तथा विपरीत निहितार्थ का रूप भी प्रस्तावित होता है। सिस्टम P के अनुरूप सिद्धांत T के उपयुक्त [[मॉडल (तर्क)|मॉडल (लॉजिक)]] का निर्माण करके प्रमाण प्रणाली P में प्रमाण के आकार पर निचली सीमा प्राप्त करना संभव है। यह [[मॉडल-सैद्धांतिक]] निर्माणों के माध्यम से कॉम्पलेक्सिटी की निचली सीमा को सिद्ध करने की अनुमति देता है, तथा दृष्टिकोण जिसे मिक्लोस अजताई की विधि के रूप में जाना जाता है।<ref name="Ajt">{{cite book|first1=M.|last1=Ajtai|author-link1=Miklós Ajtai|chapter=The complexity of the pigeonhole principle|title=Proceedings of the IEEE 29th Annual Symposium on Foundation of Computer Science|year=1988|pages=346–355}}</ref>


== SAT सॉल्वर ==
== SAT सॉल्वर ==
Line 105: Line 105:
कुछ प्रूफ सिस्टम जैसे रेजोल्यूशन और कटिंग प्लेन व्यवहार्य इंटरपोलेशन या इसके वेरिएंट को स्वीकार करते हैं।<ref name="Kr2">{{cite journal|first1=Jan|last1=Krajíček|title=अंतर्वेशन प्रमेय, प्रमाण प्रणालियों के लिए निचली सीमाएं, और बंधे हुए अंकगणित के लिए स्वतंत्रता परिणाम|journal=Journal of Symbolic Logic|volume=62|number=2|year=1997|pages=69–83|doi=10.2307/2275541|jstor=2275541}}</ref><ref name="Pu1">{{cite journal|first1=Pavel|last1=Pudlák|author-link1=Pavel Pudlak|title=रिज़ॉल्यूशन और कटिंग प्लेन प्रूफ़ और मोनोटोन गणना के लिए निचली सीमाएं|journal=Journal of Symbolic Logic|volume=62|number=3|year=1997|pages=981–998|doi=10.2307/2275583|jstor=2275583}}</ref>
कुछ प्रूफ सिस्टम जैसे रेजोल्यूशन और कटिंग प्लेन व्यवहार्य इंटरपोलेशन या इसके वेरिएंट को स्वीकार करते हैं।<ref name="Kr2">{{cite journal|first1=Jan|last1=Krajíček|title=अंतर्वेशन प्रमेय, प्रमाण प्रणालियों के लिए निचली सीमाएं, और बंधे हुए अंकगणित के लिए स्वतंत्रता परिणाम|journal=Journal of Symbolic Logic|volume=62|number=2|year=1997|pages=69–83|doi=10.2307/2275541|jstor=2275541}}</ref><ref name="Pu1">{{cite journal|first1=Pavel|last1=Pudlák|author-link1=Pavel Pudlak|title=रिज़ॉल्यूशन और कटिंग प्लेन प्रूफ़ और मोनोटोन गणना के लिए निचली सीमाएं|journal=Journal of Symbolic Logic|volume=62|number=3|year=1997|pages=981–998|doi=10.2307/2275583|jstor=2275583}}</ref>


व्यवहार्य इंटरपोलेशन को स्वचालितता के अशक्त रूप के रूप में देखा जा सकता है। वास्तव में, कई प्रमाण प्रणालियों के लिए, जैसे कि एक्सटेंडेड फ़्रीज, व्यवहार्य इंटरपोलेशन अशक्त स्वचालितता के समान है। विशेष रूप से, कई प्रमाण प्रणालियाँ P अपनी स्वयं की सुदृढ़ता सिद्ध करने में सक्षम हैं, जो टॉटोलॉजी <math>\mathrm{Ref}_P(\pi,\phi,x)</math> है जिसमें कहा गया है कि 'यदि <math>\pi</math> सूत्र <math>\phi(x)</math> का P-प्रूफ है तो <math>\phi(x)</math> मान्य है। यहाँ, <math>\pi,\phi,x</math> मुक्त चर द्वारा एन्कोड किए गए हैं। इसके अतिरिक्त, P-प्रूफ़ उत्पन्न करना संभव है <math>\mathrm{Ref}_P(\pi,\phi,x)</math> बहुपद-समय में की लंबाई दी गई है <math>\pi</math> और <math>\phi</math>. इसलिए, पी की सुदृढ़ता के लघु पी-प्रमाणों से उत्पन्न कुशल इंटरपोलेंट यह तय करेगा कि क्या कोई दिया गया सूत्र है <math>\phi</math> संक्षिप्त पी-प्रूफ़ स्वीकार करता है <math>\pi</math>. इस तरह के इंटरपोलेंट का उपयोग प्रूफ सिस्टम R को परिभाषित करने के लिए किया जा सकता है जो दर्शाता है कि पी कमजोर रूप से स्वचालित है।<ref name="PuNPpairs">{{cite journal|first1=Pavel|last1=Pudlák|author-link1=Pavel Pudlak|title=असंयुक्त एनपी-जोड़ों की न्यूनता और समरूपता पर|journal=Theoretical Computer Science|volume=295|year=2003|pages=323–339|doi=10.2307/2275583|jstor=2275583}}</ref> दूसरी ओर, प्रमाण प्रणाली पी की कमजोर स्वचालितता का तात्पर्य है कि पी व्यवहार्य इंटरपोलेशन को स्वीकार करता है। यद्यपि, यदि कोई प्रूफ सिस्टम पी अपनी स्वयं की सुदृढ़ता को कुशलता से सिद्ध नहीं करता है, तो यह व्यवहार्य इंटरपोलेशन को स्वीकार करने पर भी कमजोर रूप से स्वचालित नहीं हो सकता है।
व्यवहार्य इंटरपोलेशन को स्वचालितता के अशक्त रूप के रूप में देखा जा सकता है। वास्तव में, कई प्रमाण प्रणालियों के लिए, जैसे कि एक्सटेंडेड फ़्रीज, व्यवहार्य इंटरपोलेशन अशक्त स्वचालितता के समान है। विशेष रूप से, कई प्रमाण प्रणालियाँ P अपनी स्वयं की सुदृढ़ता सिद्ध करने में सक्षम हैं, जो टॉटोलॉजी <math>\mathrm{Ref}_P(\pi,\phi,x)</math> है जिसमें कहा गया है कि 'यदि <math>\pi</math> सूत्र <math>\phi(x)</math> का P-प्रूफ है तो <math>\phi(x)</math> मान्य है। यहाँ, <math>\pi,\phi,x</math> मुक्त चर द्वारा एन्कोड किए गए हैं। इसके अतिरिक्त, <math>\pi</math> और <math>\phi</math> की लंबाई को देखते हुए बहुपद-समय में <math>\mathrm{Ref}_P(\pi,\phi,x)</math> के P-प्रमाण उत्पन्न करना संभव है। इसलिए, P की सुदृढ़ता के लघु P-प्रमाणों से उत्पन्न कुशल इंटरपोलेंट यह निश्चित करेगा कि क्या दिया गया सूत्र <math>\phi</math> लघु पी-प्रमाण <math>\pi</math> को स्वीकार करता है। इस प्रकार के इंटरपोलेंट का उपयोग प्रूफ सिस्टम R को परिभाषित करने के लिए किया जा सकता है जो दर्शाता है कि P अशक्त रूप से स्वचालित है।<ref name="PuNPpairs">{{cite journal|first1=Pavel|last1=Pudlák|author-link1=Pavel Pudlak|title=असंयुक्त एनपी-जोड़ों की न्यूनता और समरूपता पर|journal=Theoretical Computer Science|volume=295|year=2003|pages=323–339|doi=10.2307/2275583|jstor=2275583}}</ref> दूसरी ओर, प्रमाण प्रणाली P की अशक्त स्वचालितता का तात्पर्य है कि P व्यवहार्य इंटरपोलेशन को स्वीकार करता है। यद्यपि, यदि कोई प्रूफ सिस्टम P अपनी स्वयं की सुदृढ़ता को कुशलता से सिद्ध नहीं करता है, तो यह व्यवहार्य इंटरपोलेशन को स्वीकार करने पर भी अशक्त रूप से स्वचालित नहीं हो सकता है।


कई गैर-स्वचालितता परिणाम संबंधित प्रणालियों में व्यवहार्य इंटरपोलेशन के विरुद्ध साक्ष्य प्रदान करते हैं।
कई गैर-स्वचालितता परिणाम संबंधित प्रणालियों में व्यवहार्य इंटरपोलेशन के विरुद्ध साक्ष्य प्रदान करते हैं।


* क्रेजीसेक और पुडलक (1998) ने सिद्ध किया कि ्सटेंडेड फ्रीज तब तक व्यवहार्य इंटरपोलेशन को स्वीकार नहीं करता जब तक कि आरएसए P/poly के विरुद्ध सुरक्षित न हो।<ref name="KPb">{{cite journal|first1=Jan|last1=Krajíček|first2=Pavel|last2=Pudlák|author-link2=Pavel Pudlak|title=Some consequences of cryptographical conjectures for <math>S^1_2</math> and EF|journal=Information and Computation|volume=140|number=1|year=1998|pages=82–94|doi=10.1006/inco.1997.2674|doi-access=free}}</ref>
* क्रेजीसेक और पुडलक (1998) ने सिद्ध किया कि एक्सटेंडेड फ्रीज तब तक व्यवहार्य इंटरपोलेशन को स्वीकार नहीं करता जब तक कि आरएसए P/poly के विरुद्ध सुरक्षित न हो।<ref name="KPb">{{cite journal|first1=Jan|last1=Krajíček|first2=Pavel|last2=Pudlák|author-link2=Pavel Pudlak|title=Some consequences of cryptographical conjectures for <math>S^1_2</math> and EF|journal=Information and Computation|volume=140|number=1|year=1998|pages=82–94|doi=10.1006/inco.1997.2674|doi-access=free}}</ref>
* बोनेट, पिटासी और रज़ (2000) ने सिद्ध किया कि <math>TC^0</math>-फ्रेज सिस्टम तब तक व्यवहार्य इंटरपोलेशन को स्वीकार नहीं करता जब तक कि डिफी-हेलमैन योजना P/poly के विरुद्ध सुरक्षित न हो।<ref name="BPRb">{{cite journal|first1=M.L.|last1=Bonet|author-link1=M.L. Bonet|first2=Toniann|last2=Pitassi|author-link2=Toniann Pitassi|first3=Ran|last3=Raz|author-link3=Ran Raz|title=फ्रीज प्रूफ सिस्टम के लिए इंटरपोलेशन और ऑटोमेशन पर|journal=SIAM Journal on Computing|volume=29|number=6|year=2000|pages=1939–1967|doi=10.1137/S0097539798353230}}</ref>
* बोनेट, पिटासी और रज़ (2000) ने सिद्ध किया कि <math>TC^0</math>-फ्रेज सिस्टम तब तक व्यवहार्य इंटरपोलेशन को स्वीकार नहीं करता जब तक कि डिफी-हेलमैन योजना P/poly के विरुद्ध सुरक्षित न हो।<ref name="BPRb">{{cite journal|first1=M.L.|last1=Bonet|author-link1=M.L. Bonet|first2=Toniann|last2=Pitassi|author-link2=Toniann Pitassi|first3=Ran|last3=Raz|author-link3=Ran Raz|title=फ्रीज प्रूफ सिस्टम के लिए इंटरपोलेशन और ऑटोमेशन पर|journal=SIAM Journal on Computing|volume=29|number=6|year=2000|pages=1939–1967|doi=10.1137/S0097539798353230}}</ref>
* बोनेट, डोमिंगो, गवाल्डा, मैकिएल, पिटासी (2004) ने सिद्ध कर दिया कि स्थिर-गहराई वाले फ़्रीज सिस्टम तब तक व्यवहार्य इंटरपोलेशन को स्वीकार नहीं करते हैं जब तक कि डिफी-हेलमैन योजना उप-घातीय समय में कार्य करने वाले गैर-समान विरोधियों के विरुद्ध सुरक्षित न हो।<ref name="BDGMPb">{{cite journal|first1=M.L.|last1=Bonet|author-link1=M.L. Bonet|first2=C.|last2=Domingo|first3=R.|last3=Gavaldá|first4=A.|last4=Maciel|first5=Toniann|last5=Pitassi|s2cid=1360759|author-link5=Toniann Pitassi|title=बाउंडेड-डेप्थ फ़्रीज प्रूफ़ की गैर-स्वचालितता|journal=Computational Complexity|volume=13|year=2004|issue=1–2|pages=47–68|doi=10.1007/s00037-004-0183-5}}</ref>
* बोनेट, डोमिंगो, गवाल्डा, मैकिएल, पिटासी (2004) ने सिद्ध कर दिया कि स्थिर-डेप्थ वाले फ़्रीज सिस्टम तब तक व्यवहार्य इंटरपोलेशन को स्वीकार नहीं करते हैं जब तक कि डिफी-हेलमैन योजना उप-घातीय समय में कार्य करने वाले असमान विरोधियों के विरुद्ध सुरक्षित न हो।<ref name="BDGMPb">{{cite journal|first1=M.L.|last1=Bonet|author-link1=M.L. Bonet|first2=C.|last2=Domingo|first3=R.|last3=Gavaldá|first4=A.|last4=Maciel|first5=Toniann|last5=Pitassi|s2cid=1360759|author-link5=Toniann Pitassi|title=बाउंडेड-डेप्थ फ़्रीज प्रूफ़ की गैर-स्वचालितता|journal=Computational Complexity|volume=13|year=2004|issue=1–2|pages=47–68|doi=10.1007/s00037-004-0183-5}}</ref>


== [[गैर-शास्त्रीय तर्क]] ==
== [[गैर-शास्त्रीय तर्क|नॉन-क्लासिकल लॉजिक]] ==
प्रमाणों के आकार की तुलना करने के विचार का उपयोग किसी भी स्वचालित तर्क प्रक्रिया के लिए किया जा सकता है जो प्रमाण उत्पन्न करती है। प्रस्तावात्मक गैर-शास्त्रीय तर्क, विशेष रूप से [[अंतर्ज्ञानवादी तर्क]], [[मोडल तर्क]] और [[गैर-मोनोटोनिक तर्क]] के लिए प्रमाणों के आकार के बारे में कुछ शोध किए गए हैं।
प्रमाणों के आकार की उपमा करने के विचार का उपयोग किसी भी स्वचालित लॉजिक प्रक्रिया के लिए किया जा सकता है जो प्रमाण उत्पन्न करती है। प्रोपोज़िशनल नॉन-क्लासिकल लॉजिक, विशेष रूप से [[अंतर्ज्ञानवादी तर्क|इंटुइशनिस्टिक लॉजिक]], [[मोडल तर्क|मोडल लॉजिक]] और [[गैर-मोनोटोनिक तर्क|नॉन-मोनोटोनिक लॉजिक]] के लिए प्रमाणों के आकार के संबंध में कुछ शोध किए गए हैं।


ह्रुबेस (2007-2009) ने कुछ मोडल लॉजिक्स में और मोनोटोन व्यवहार्य इंटरपोलेशन के संस्करण का उपयोग करके अंतर्ज्ञानवादी तर्क में एक्सटेंडेड फ्रीज सिस्टम में सबूतों के आकार पर घातीय निचली सीमाएं सिद्ध कीं।<ref name="Hr1">{{cite journal|first1=Pavel|last1=Hrubeš|author-link1=Pavel Hrubeš|title=मोडल लॉजिक्स के लिए निचली सीमाएं|journal=Journal of Symbolic Logic|volume=72|number=3|year=2007|pages=941–958|doi=10.2178/jsl/1191333849|s2cid=1743011}}</ref><ref name="Hr2">{{cite journal|first1=Pavel|last1=Hrubeš|author-link1=Pavel Hrubeš|title=अंतर्ज्ञानवादी तर्क के लिए एक निचली सीमा|journal=Annals of Pure and Applied Logic|volume=146|number=1|year=2007|pages=72–90|doi=10.1016/j.apal.2007.01.001|doi-access=free}}</ref><ref name="Hr3">{{cite journal|first1=Pavel|last1=Hrubeš|author-link1=Pavel Hrubeš|title=गैर-शास्त्रीय तर्कशास्त्र में प्रमाणों की लंबाई पर|journal=Annals of Pure and Applied Logic|volume=157|number=2–3|year=2009|pages=194–205|doi=10.1016/j.apal.2008.09.013|doi-access=free}}</ref>
ह्रुबेस (2007-2009) ने कुछ मोडल लॉजिक्स में और मोनोटोन व्यवहार्य इंटरपोलेशन के संस्करण का उपयोग करके इंटुइशनिस्टिक लॉजिक में एक्सटेंडेड फ्रीज सिस्टम में प्रमाणों के आकार पर घातीय निचली सीमाएं सिद्ध कीं थी।<ref name="Hr1">{{cite journal|first1=Pavel|last1=Hrubeš|author-link1=Pavel Hrubeš|title=मोडल लॉजिक्स के लिए निचली सीमाएं|journal=Journal of Symbolic Logic|volume=72|number=3|year=2007|pages=941–958|doi=10.2178/jsl/1191333849|s2cid=1743011}}</ref><ref name="Hr2">{{cite journal|first1=Pavel|last1=Hrubeš|author-link1=Pavel Hrubeš|title=अंतर्ज्ञानवादी तर्क के लिए एक निचली सीमा|journal=Annals of Pure and Applied Logic|volume=146|number=1|year=2007|pages=72–90|doi=10.1016/j.apal.2007.01.001|doi-access=free}}</ref><ref name="Hr3">{{cite journal|first1=Pavel|last1=Hrubeš|author-link1=Pavel Hrubeš|title=गैर-शास्त्रीय तर्कशास्त्र में प्रमाणों की लंबाई पर|journal=Annals of Pure and Applied Logic|volume=157|number=2–3|year=2009|pages=194–205|doi=10.1016/j.apal.2008.09.013|doi-access=free}}</ref>


== यह भी देखें ==
== यह भी देखें ==
Line 122: Line 122:
*सर्किट कॉम्पलेक्सिटी
*सर्किट कॉम्पलेक्सिटी
*[[संचार जटिलता|संचार कॉम्पलेक्सिटी]]
*[[संचार जटिलता|संचार कॉम्पलेक्सिटी]]
*गणितीय तर्क
*गणितीय लॉजिक
*प्रमाण सिद्धांत
*प्रमाण सिद्धांत
*[[जटिलता वर्ग|कॉम्पलेक्सिटी वर्ग]]
*[[जटिलता वर्ग|कॉम्पलेक्सिटी वर्ग]]
*एनपी (कॉम्पलेक्सिटी)
*NP (कॉम्पलेक्सिटी)
*सीओएनपी
*coNP


==संदर्भ==
==संदर्भ==

Revision as of 14:44, 6 August 2023

लॉजिक और सैद्धांतिक कंप्यूटर विज्ञान में, और विशेष रूप से प्रमाण सिद्धांत और कम्प्यूटेशनल कॉम्पलेक्सिटी सिद्धांत में, प्रूफ कॉम्पलेक्सिटी वह क्षेत्र है जिसका लक्ष्य उन कम्प्यूटेशनल संसाधनों का अध्ययन और उनका विश्लेषण करना है जो स्टेटमेंट्स को सिद्ध करने अथवा खंडन करने के लिए आवश्यक हैं। प्रूफ कॉम्पलेक्सिटी में अनुसंधान मुख्य रूप से विभिन्न प्रस्ताव प्रमाण प्रणालियों में प्रमाण-लंबाई की निचली और ऊपरी सीमा को सिद्ध करने से संबंधित है। उदाहरण के लिए, प्रूफ कॉम्पलेक्सिटी के प्रमुख प्रवादों में से यह दर्शाना है कि फ़्रीज सिस्टम, सामान्य प्रस्तावात्मक कलन, सभी टॉटोलॉजीज़ के बहुपद-आकार के प्रमाणों को स्वीकार नहीं करता है। यहां प्रमाण का आकार केवल उसमें प्रतीकों की संख्या है, और प्रमाण को बहुपद आकार का कहा जाता है यदि यह टॉटोलॉजी के आकार में बहुपद है जो इसे सिद्ध करता है।

प्रूफ कॉम्पलेक्सिटी का व्यवस्थित अध्ययन स्टीफन कुक और रॉबर्ट रेकहो (1979) के कार्य से प्रारम्भ हुआ, जिन्होंने कम्प्यूटेशनल कॉम्पलेक्सिटी के परिप्रेक्ष्य से प्रस्ताव प्रमाण प्रणाली की मूल परिभाषा प्रदान की थी। विशेष रूप से कुक और रेकहो ने देखा कि दृढ़ प्रोपोज़िशनल प्रूफ़ सिस्टम पर प्रूफ साइज की निचली सीमा सिद्ध करने को NP (कॉम्पलेक्सिटी) को coNP से पृथक करने की दिशा में चरण के रूप में देखा जा सकता है (और इस प्रकार NP से P (कॉम्पलेक्सिटी)), क्योंकि प्रोपोज़िशनल प्रूफ़ सिस्टम का अस्तित्व है जो बहुपद आकार के प्रमाणों को स्वीकार करता है, सभी टॉटोलॉजी के लिए NP=coNP के समान है।

समसामयिक प्रूफ कॉम्पलेक्सिटी अनुसंधान कम्प्यूटेशनल कॉम्पलेक्सिटी, कलन विधि और गणित के कई क्षेत्रों से विचार और विधियाँ प्राप्त करता है। यद्यपि कई महत्वपूर्ण एल्गोरिदम और एल्गोरिदमिक तकनीकों को कुछ प्रूफ सिस्टमों के लिए प्रूफ सर्च एल्गोरिदम के रूप में निक्षेप किया जा सकता है, इसलिए इन सिस्टमों में प्रूफ आकारों पर निचली सीमाएं सिद्ध करते हैं, इसका अर्थ है कि संबंधित एल्गोरिदम पर रन-टाइम निचली सीमाएं होती हैं। यह प्रूफ कॉम्पलेक्सिटी को SAT सॉल्वर जैसे अधिक व्यावहारिक क्षेत्रों से संयोजित करता है।

गणितीय लॉजिक प्रस्तावित प्रमाण आकारों का अध्ययन करने के लिए फ्रेमवर्क के रूप में भी कार्य कर सकता है। प्रथम-क्रम सिद्धांत और, विशेष रूप से, पीनो अंकगणित के वीक फ्रेगमेंट, जो सीमित अंकगणित के नाम से आते हैं, प्रस्ताव प्रमाण प्रणालियों के समान संस्करणों के रूप में कार्य करते हैं और व्यवहार्य लॉजिक के विभिन्न स्तरों के संदर्भ में लघु प्रस्ताव प्रमाणों की व्याख्या के लिए अग्र पृष्ठभूमि प्रदान करते हैं।

प्रमाण प्रणालियाँ

Main article: प्रोपोज़िशनल प्रूफ सिस्टम

प्रोपोज़िशनल प्रूफ सिस्टम को दो इनपुट के साथ प्रमाण-सत्यापन एल्गोरिथ्म P(A,x) के रूप में दिया गया है। यदि P पेयर (A,x) को स्वीकार करता है तो हम कहते हैं कि x, A का P-प्रूफ है। P को बहुपद समय में रन करना आवश्यक है, और इसके अतिरिक्त यह मानना ​​होगा कि A के निकट P-प्रूफ है यदि A टॉटोलॉजी है।

प्रोपोज़िशनल प्रूफ सिस्टम के उदाहरणों में अनुक्रमिक कलन, रिज़ॉल्यूशन (लॉजिक), कटिंग-प्लेन विधि और फ़्रीज सिस्टम सम्मिलित हैं। ज़र्मेलो फ्रेंकेल सेट सिद्धांत जैसे दृढ़ गणितीय सिद्धांत प्रस्तावात्मक प्रमाण प्रणालियों को भी प्रेरित करते हैं: ZFC की प्रस्तावात्मक व्याख्या में टॉटोलॉजी का प्रमाण औपचारिक कथन ' टॉटोलॉजी है' का ZFC-प्रमाण है।

बहुपद आकार के प्रमाण और NP के प्रति coNP समस्या

प्रूफ़ कॉम्पलेक्सिटी सामान्यतः किसी दिए गए टॉटोलॉजी के लिए सिस्टम में संभव प्रूफ़ों के न्यूनतम आकार के संदर्भ में प्रूफ़ प्रणाली की दक्षता को मापती है। प्रमाण का आकार (क्रमशः सूत्र) प्रमाण (क्रमशः सूत्र) का प्रतिनिधित्व करने के लिए आवश्यक प्रतीकों की संख्या है। प्रस्ताव प्रमाण प्रणाली P बहुपद रूप से परिबद्ध होती है यदि इसमें स्थिरांक उपस्थित होता है जैसे कि आकार के प्रत्येक टॉटोलॉजी में आकार का P-प्रूफ होता है। प्रूफ कॉम्पलेक्सिटी का केंद्रीय प्रश्न यह समझना है कि क्या टॉटोलॉजी बहुपद-आकार के प्रमाणों को स्वीकार करती है। औपचारिक रूप से,

समस्या (NP के प्रति coNP)

क्या बहुपद से परिबद्ध प्रस्तावात्मक प्रमाण प्रणाली उपस्थित है?

कुक और रेकहो (1979) ने देखा कि बहुपद रूप से परिबद्ध प्रमाण प्रणाली उपस्थित है यदि NP=coNP है। इसलिए, यह सिद्ध करना कि विशिष्ट प्रमाण प्रणालियाँ बहुपद आकार के प्रमाणों को स्वीकार नहीं करती हैं, इसे NP और coNP (और इस प्रकार P और NP) को पृथक करने की दिशा में आंशिक प्रगति के रूप में देखा जा सकता है।[1]

प्रूफ सिस्टम के मध्य इष्टतमता और सिमुलेशन

प्रूफ कॉम्पलेक्सिटी सिमुलेशन की धारणा का उपयोग करके प्रूफ सिस्टम के सामर्थ्य की उपमा करती है। प्रूफ सिस्टम P, p-प्रूफ सिस्टम Q का अनुकरण करता है यदि कोई बहुपद-समय फ़ंक्शन है जो टॉटोलॉजी का Q-प्रूफ देता है तो उसी टॉटोलॉजी का P-प्रूफ आउटपुट करता है। यदि P, p-Q का अनुकरण करता है और Q, p-P का अनुकरण करता है, तो प्रमाण प्रणाली P और Q, p-समतुल्य हैं। सिमुलेशन की अशक्त धारणा भी है: प्रूफ सिस्टम P प्रूफ सिस्टम Q का अनुकरण करता है यदि कोई बहुपद p है जैसे कि टॉटोलॉजी A के प्रत्येक Q-प्रूफ़ x के लिए, A का P-प्रूफ y है जैसे कि y की लंबाई, |y| अधिकतम p(|x|) है।

उदाहरण के लिए, अनुक्रमिक कलन (प्रत्येक) फ़्रीज सिस्टम के लिए p-समतुल्य है।[2]

प्रूफ सिस्टम p-इष्टतम है यदि यह अन्य सभी प्रूफ सिस्टमों का p-अनुकरण करता है, और यह इष्टतम है यदि यह अन्य सभी प्रूफ सिस्टमों का अनुकरण करता है। यह संवृत समस्या है कि क्या ऐसी प्रमाण प्रणालियाँ उपस्थित हैं:

समस्या (इष्टतमता)

क्या कोई p-इष्टतम या इष्टतम प्रस्तावक प्रमाण प्रणाली उपस्थित है?

प्रत्येक प्रस्तावित प्रमाण प्रणाली P को P की सुदृढ़ता को अभिगृहीत करने वाले सिद्धांतों के साथ विस्तारित फ़्रीज द्वारा अनुकरण किया जा सकता है।[3] इष्टतम (क्रमशः p-इष्टतम) प्रमाण प्रणाली का अस्तित्व इस धारणा से जाना जाता है कि NE=coNE (क्रमशः E (कॉम्पलेक्सिटी)=NE (कॉम्पलेक्सिटी)) है।[4]

कई वीक प्रूफ सिस्टमों के लिए यह ज्ञात है कि वे कुछ दृढ़ प्रणालियों का अनुकरण नहीं करते हैं (नीचे देखें)। यद्यपि, यदि अनुकरण की धारणा को शिथिल कर दिया जाए तो यह प्रश्न संवृत रहता है। उदाहरण के लिए, यह संवृत है कि क्या रिज़ॉल्यूशन प्रभावी रूप से बहुपद रूप से विस्तारित फ़्रीज का अनुकरण करता है।[5]

प्रूफ सर्च की स्वचालितता

प्रूफ कॉम्पलेक्सिटी में महत्वपूर्ण प्रश्न प्रमाण प्रणालियों में प्रूफ सर्च की कॉम्पलेक्सिटी का अध्ययन करना है।

समस्या (स्वचालितता)

क्या रेजोल्यूशन अथवा फ़्रीज सिस्टम जैसे मानक प्रूफ सिस्टम में प्रूफ सर्च करने के लिए कुशल एल्गोरिदम हैं?

प्रश्न को स्वचालितता (जिसे स्वचालितता के रूप में भी जाना जाता है) की धारणा द्वारा औपचारिक रूप दिया जा सकता है।[6]

प्रूफ सिस्टम P स्वचालित है यदि कोई एल्गोरिदम है जो टॉटोलॉजी देता है तो के आकार में समय बहुपद में का P-प्रूफ आउटपुट करता है और के सबसे छोटे P-प्रूफ की लंबाई होती है। ध्यान दें कि यदि कोई प्रूफ सिस्टम बहुपद से परिबद्ध नहीं है, तब भी यह स्वचालित हो सकता है। प्रूफ सिस्टम P अशक्त रूप से स्वचालित है यदि प्रूफ सिस्टम R और एल्गोरिदम है जिसे टॉटोलॉजी दिया गया है जो के आकार में समय बहुपद में का R-प्रूफ आउटपुट करता है और के सबसे छोटे P-प्रूफ की लंबाई है।

माना जाता है कि ब्याज की कई प्रमाण प्रणालियाँ गैर-स्वचालित हैं। यद्यपि, वर्तमान में केवल प्रतिबंधात्मक नकारात्मक परिणाम ही ज्ञात हैं।

  • क्रेजीसेक और पुडलक (1998) ने सिद्ध किया कि एक्सटेंडेड फ्रीज तब तक अशक्त रूप से स्वचालित नहीं है जब तक कि आरएसए एन्क्रिप्शन P/poly के विरुद्ध सुरक्षित न हो।[7]
  • मारिया लुइसा बोनेट, टोनियान पिटासी और रेज़ (2000) ने सिद्ध किया कि -फ्रेज सिस्टम अशक्त रूप से स्वचालित नहीं है जब तक कि कुंजी विनिमय अथवा डिफी-हेलमैन योजना P/poly के विरुद्ध सुरक्षित न हो।[8] इसे बोनेट, डोमिंगो, गवाल्डा, मैकिएल और पिटासी (2004) द्वारा विस्तारित किया गया था, जिन्होंने सिद्ध किया कि कम से कम 2 गहराई की फ़्रीज़ प्रणालियाँ तब तक अशक्त रूप से स्वचालित नहीं होती हैं जब तक कि डिफी-हेलमैन योजना उप-घातीय समय में कार्य करने वाले असमान विरोधियों के विरुद्ध सुरक्षित न हो।[9]
  • अलेख्नोविच और रज़बोरोव (2008) ने सिद्ध किया कि ट्री जैसे रिज़ॉल्यूशन और रिज़ॉल्यूशन तब तक स्वचालित नहीं होते जब तक कि पैरामीटरयुक्त कॉम्पलेक्सिटी FPT=W[P] न हो।[10] इसे गैलेसी और लौरिया (2010) द्वारा विस्तारित किया गया था, जिन्होंने सिद्ध किया कि जब तक निश्चित-पैरामीटर पदानुक्रम ध्वस्त नहीं हो जाता, तब तक शून्य प्रमेय और पॉलीनोमियल कलन स्वचालित नहीं होते हैं।[11] मर्ट्ज़, पिटासी और वेई (2019) ने सिद्ध कर दिया कि घातीय समय परिकल्पना को मानते हुए ट्री जैसे रिज़ॉल्यूशन और रिज़ॉल्यूशन कुछ अर्ध-बहुपद समय में भी स्वचालित नहीं होते हैं।[12]
  • एटसेरियस और मुलर (2019) ने सिद्ध कर दिया कि रिज़ॉल्यूशन तब तक स्वचालित नहीं है जब तक कि P=NP न हो।[13] इसे डी रेज़ेंडे, गूस, नॉर्डस्ट्रॉम, पिटासी, रोबेरे और सोकोलोव (2020) द्वारा नलस्टेलेंसैट्ज़ और पॉलीनोमियल कलन को स्वचालित करने की NP-कठोरता तक विस्तारित किया गया था;[14] इसे गोओस, कोरोथ, मर्ट्ज़ और पिटासी (2020) द्वारा कटिंग प्लेनों को स्वचालित करने की NP-कठोरता तक विस्तारित किया गया था;[15] तथा गार्लिक (2020) द्वारा के-डिसजंक्टिव सामान्य फॉर्म रिज़ॉल्यूशन को स्वचालित करने की NP-कठोरता तक भी विस्तारित किया गया था।[16]

यह ज्ञात नहीं है कि रिज़ॉल्यूशन की अशक्त स्वचालितता किसी भी मानक कॉम्पलेक्सिटी-सैद्धांतिक कठोरता की धारणाओं को खंडित करेगी या नहीं करेगी।

सकारात्मक पक्ष पर,

  • बीम और पिटासी (1996) ने दर्शाया कि ट्री जैसा रिज़ॉल्यूशन अर्ध-बहुपद समय में स्वचालित होता है और रिज़ॉल्यूशन अशक्त उप-घातीय समय में स्माल विड्थ के सूत्रों पर स्वचालित होता है।[17][18]

परिबद्ध अंकगणित

Main article: परिबद्ध अंकगणित

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

पत्राचार स्टीफन कुक (1975) द्वारा प्रस्तुत किया गया था, जिन्होंने दिखाया के सीओएनपी प्रमेय, औपचारिक रूप से सूत्र, विस्तारित फ़्रीज में बहुपद-आकार के प्रमाणों के साथ टॉटोलॉजी के अनुक्रम में अनुवाद करते हैं। इसके अतिरिक्त, एक्सटेंडेड फ्रीज इस प्रकार की सबसे अशक्त प्रणाली है: यदि किसी अन्य प्रूफ सिस्टम P में यह गुण है, तो P एक्सटेंडेड फ्रीज का अनुकरण करता है।[19]

जेफ पेरिस (गणितज्ञ) और एलेक्स विल्की (1985) द्वारा दिए गए द्वितीय क्रम के स्टेटमेंट्स और प्रस्तावित सूत्रों के मध्य वैकल्पिक अनुवाद एक्सटेंडेड फ्रीज जैसे फ्रीज अथवा निरंतर-डेप्थ फ्रीज के सबसिस्टम्स को कैप्चर करने के लिए अधिक व्यावहारिक रहा है।[20][21]

जबकि उपर्युक्त पत्राचार कहता है कि सिद्धांत में प्रमाण संबंधित प्रमाण प्रणाली में लघु प्रमाणों के अनुक्रम में परिवर्तन हो जाता है, तथा विपरीत निहितार्थ का रूप भी प्रस्तावित होता है। सिस्टम P के अनुरूप सिद्धांत T के उपयुक्त मॉडल (लॉजिक) का निर्माण करके प्रमाण प्रणाली P में प्रमाण के आकार पर निचली सीमा प्राप्त करना संभव है। यह मॉडल-सैद्धांतिक निर्माणों के माध्यम से कॉम्पलेक्सिटी की निचली सीमा को सिद्ध करने की अनुमति देता है, तथा दृष्टिकोण जिसे मिक्लोस अजताई की विधि के रूप में जाना जाता है।[22]

SAT सॉल्वर

See also: SAT सॉल्वर

टॉटोलॉजी को पहचानने के लिए प्रपोजल प्रूफ सिस्टम की व्याख्या अनियतात्मक एल्गोरिदम के रूप में की जा सकती है। प्रमाण प्रणाली P पर सुपरपोलिनोमियल निचली सीमा सिद्ध करना इस प्रकार P के आधार पर SAT के लिए बहुपद-समय एल्गोरिदम के अस्तित्व को अस्वीकृत कर देता है। उदाहरण के लिए, असंतोषजनक उदाहरणों पर डीपीएलएल एल्गोरिदम का रन ट्री-जैसे रिज़ॉल्यूशन खंडन के अनुरूप होता है। इसलिए, ट्री-जैसे रिज़ॉल्यूशन (नीचे देखें) के लिए घातीय निचली सीमाएं SAT के लिए कुशल डीपीएलएल एल्गोरिदम के अस्तित्व को अस्वीकृत करती हैं। इसी प्रकार, घातीय रिज़ॉल्यूशन निचली सीमा का अर्थ है कि रिज़ॉल्यूशन पर आधारित SAT सॉल्वर, जैसे कि कॉनफ्लिक्ट-ड्राइवन क्लॉज लर्निंग एल्गोरिदम, SAT को कुशलतापूर्वक हल नहीं कर सकते हैं।

निचली सीमा

प्रस्तावित प्रमाणों की लंबाई पर निचली सीमा सिद्ध करना सामान्यतः कठिन होता है। तत्पश्चात, वीक प्रूफ सिस्टम के लिए निचली सीमा सिद्ध करने की कई विधियाँ ज्ञात की गयी हैं।

  • हेकेन (1985) ने रिज़ॉल्यूशन और पिजनहोल सिद्धांत के लिए एक्सपोनेंशियल लोअर बाउंड सिद्ध को सिद्ध किया था।[23]
  • अजताई (1988) ने स्थिर-डेप्थ वाले फ़्रीज सिस्टम और पिजनहोल सिद्धांत के लिए सुपरपोलिनोमियल निचली सीमा सिद्ध की थी।[24] इसे क्रेजीसेक, पुडलक और वुड्स और पिटासी, बीम और इम्पाग्लियाज़ो द्वारा[25] एक्सपोनेंशियल लोअर बाउंड तक दृढ़ किया गया था।[26] अजताई की निचली सीमा यादृच्छिक प्रतिबंधों की विधि का उपयोग करती है, जिसका उपयोग सर्किट कॉम्पलेक्सिटी में AC0 निचली सीमा प्राप्त करने के लिए भी किया जाता था।
  • क्राजिएक (1994)[27] ने व्यवहार्य इंटरपोलेशन की विधि प्रस्तुत की, जिसके पश्चात इसका उपयोग रिज़ॉल्यूशन और अन्य प्रमाण प्रणालियों के लिए नई निचली सीमाएँ प्राप्त करने के लिए किया।[28]
  • पुडलक (1997) ने व्यवहार्य इंटरपोलेशन के माध्यम से तलों को विभक्त करने के लिए एक्सपोनेंशियल लोअर बाउंड को सिद्ध किया था।[29]
  • बेन-सैसन और विगडरसन (1999) ने रिज़ॉल्यूशन खंडन के आकार की निचली सीमा को कम करके रिज़ॉल्यूशन खंडन की विड्थ की निचली सीमा तक प्रमाण विधि प्रदान की, जिसने हेकेन की निचली सीमा के कई सामान्यीकरणों को कैप्चर कर लिया था।[18]

फ़्रीज सिस्टम के लिए गैर-तुच्छ निचली सीमा प्राप्त करना अधिक समय से चली आ रही संवृत समस्या है।

व्यवहार्य इंटरपोलेशन

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

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

कुछ प्रूफ सिस्टम जैसे रेजोल्यूशन और कटिंग प्लेन व्यवहार्य इंटरपोलेशन या इसके वेरिएंट को स्वीकार करते हैं।[28][29]

व्यवहार्य इंटरपोलेशन को स्वचालितता के अशक्त रूप के रूप में देखा जा सकता है। वास्तव में, कई प्रमाण प्रणालियों के लिए, जैसे कि एक्सटेंडेड फ़्रीज, व्यवहार्य इंटरपोलेशन अशक्त स्वचालितता के समान है। विशेष रूप से, कई प्रमाण प्रणालियाँ P अपनी स्वयं की सुदृढ़ता सिद्ध करने में सक्षम हैं, जो टॉटोलॉजी है जिसमें कहा गया है कि 'यदि सूत्र का P-प्रूफ है तो मान्य है। यहाँ, मुक्त चर द्वारा एन्कोड किए गए हैं। इसके अतिरिक्त, और की लंबाई को देखते हुए बहुपद-समय में के P-प्रमाण उत्पन्न करना संभव है। इसलिए, P की सुदृढ़ता के लघु P-प्रमाणों से उत्पन्न कुशल इंटरपोलेंट यह निश्चित करेगा कि क्या दिया गया सूत्र लघु पी-प्रमाण को स्वीकार करता है। इस प्रकार के इंटरपोलेंट का उपयोग प्रूफ सिस्टम R को परिभाषित करने के लिए किया जा सकता है जो दर्शाता है कि P अशक्त रूप से स्वचालित है।[30] दूसरी ओर, प्रमाण प्रणाली P की अशक्त स्वचालितता का तात्पर्य है कि P व्यवहार्य इंटरपोलेशन को स्वीकार करता है। यद्यपि, यदि कोई प्रूफ सिस्टम P अपनी स्वयं की सुदृढ़ता को कुशलता से सिद्ध नहीं करता है, तो यह व्यवहार्य इंटरपोलेशन को स्वीकार करने पर भी अशक्त रूप से स्वचालित नहीं हो सकता है।

कई गैर-स्वचालितता परिणाम संबंधित प्रणालियों में व्यवहार्य इंटरपोलेशन के विरुद्ध साक्ष्य प्रदान करते हैं।

  • क्रेजीसेक और पुडलक (1998) ने सिद्ध किया कि एक्सटेंडेड फ्रीज तब तक व्यवहार्य इंटरपोलेशन को स्वीकार नहीं करता जब तक कि आरएसए P/poly के विरुद्ध सुरक्षित न हो।[31]
  • बोनेट, पिटासी और रज़ (2000) ने सिद्ध किया कि -फ्रेज सिस्टम तब तक व्यवहार्य इंटरपोलेशन को स्वीकार नहीं करता जब तक कि डिफी-हेलमैन योजना P/poly के विरुद्ध सुरक्षित न हो।[32]
  • बोनेट, डोमिंगो, गवाल्डा, मैकिएल, पिटासी (2004) ने सिद्ध कर दिया कि स्थिर-डेप्थ वाले फ़्रीज सिस्टम तब तक व्यवहार्य इंटरपोलेशन को स्वीकार नहीं करते हैं जब तक कि डिफी-हेलमैन योजना उप-घातीय समय में कार्य करने वाले असमान विरोधियों के विरुद्ध सुरक्षित न हो।[33]

नॉन-क्लासिकल लॉजिक

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

ह्रुबेस (2007-2009) ने कुछ मोडल लॉजिक्स में और मोनोटोन व्यवहार्य इंटरपोलेशन के संस्करण का उपयोग करके इंटुइशनिस्टिक लॉजिक में एक्सटेंडेड फ्रीज सिस्टम में प्रमाणों के आकार पर घातीय निचली सीमाएं सिद्ध कीं थी।[34][35][36]

यह भी देखें

संदर्भ

  1. ↑ Cook, Stephen; Reckhow, Robert A. (1979). "प्रस्तावक प्रमाण प्रणालियों की सापेक्ष दक्षता". Journal of Symbolic Logic. 44 (1): 36–50. doi:10.2307/2273702. JSTOR 2273702.
  2. ↑ Reckhow, Robert A. (1976). प्रस्तावात्मक गणना में प्रमाणों की लंबाई पर (PhD Thesis). University of Toronto.
  3. ↑ Krajíček, Jan (2019). प्रमाण जटिलता. Cambridge University Press.
  4. ↑ Krajíček, Jan; Pudlák, Pavel (1989). "प्रस्तावात्मक प्रमाण प्रणालियाँ, प्रथम-क्रम सिद्धांतों की संगति और संगणना की जटिलता". Journal of Symbolic Logic. 54 (3): 1063–1079. doi:10.2307/2274765. JSTOR 2274765.
  5. ↑ Pitassi, Toniann; Santhanam, Rahul (2010). "प्रभावी ढंग से बहुपद सिमुलेशन" (PDF). ICS: 370–382.
  6. ↑ Bonet, M.L.; Pitassi, Toniann; Raz, Ran (2000). "फ्रीज प्रूफ सिस्टम के लिए इंटरपोलेशन और ऑटोमेशन पर". SIAM Journal on Computing. 29 (6): 1939–1967. doi:10.1137/S0097539798353230.
  7. ↑ Krajíček, Jan; Pudlák, Pavel (1998). "Some consequences of cryptographical conjectures for and EF". Information and Computation. 140 (1): 82–94. doi:10.1006/inco.1997.2674.
  8. ↑ Bonet, M.L.; Pitassi, Toniann; Raz, Ran (2000). "फ्रीज प्रूफ सिस्टम के लिए इंटरपोलेशन और ऑटोमेशन पर". SIAM Journal on Computing. 29 (6): 1939–1967. doi:10.1137/S0097539798353230.
  9. ↑ Bonet, M.L.; Domingo, C.; Gavaldá, R.; Maciel, A.; Pitassi, Toniann (2004). "बाउंडेड-डेप्थ फ़्रीज प्रूफ़ की गैर-स्वचालितता". Computational Complexity. 13 (1–2): 47–68. doi:10.1007/s00037-004-0183-5. S2CID 1360759.
  10. ↑ Alekhnovich, Michael; Razborov, Alexander (2018). "Resolution is not automatizable unless W[P] is tractable". SIAM Journal on Computing. 38 (4): 1347–1363. doi:10.1137/06066850X.
  11. ↑ Galesi, Nicola; Lauria, Massimo (2010). "बहुपद कलन की स्वचालितता पर". Theory of Computing Systems. 47 (2): 491–506. doi:10.1007/s00224-009-9195-5. S2CID 11602606.
  12. ↑ Mertz, Ian; Pitassi, Toniann; Wei, Yuanhao (2019). "लघु प्रमाण खोजना कठिन है". ICALP.
  13. ↑ Atserias, Albert; Müller, Moritz (2019). "Automating resolution is NP-hard". Proceedings of the 60th Symposium on Foundations of Computer Science. pp. 498–509.
  14. ↑ de Rezende, Susanna; Göös, Mika; Nordström, Jakob; Pitassi, Tonnian; Robere, Robert; Sokolov, Dmitry (2020). "बीजगणितीय प्रमाण प्रणालियों को स्वचालित करना एनपी-हार्ड है". ECCC.
  15. ↑ Göös, Mika; Koroth, Sajin; Mertz, Ian; Pitassi, Tonnian (2020). "कटिंग विमानों को स्वचालित करना एनपी-हार्ड है". STOC: 68–77. arXiv:2004.08037. doi:10.1145/3357713.3384248. ISBN 9781450369794. S2CID 215814356.
  16. ↑ Garlík, Michal (2020). "के-डीएनएफ रिज़ॉल्यूशन और इसे स्वचालित करने की एनपी-कठोरता के लिए व्यवहार्य विच्छेदन संपत्ति की विफलता". ECCC. arXiv:2003.10230.
  17. ↑ Beame, Paul; Pitassi, Toniann (1996). "सरलीकृत और बेहतर रिज़ॉल्यूशन निचली सीमाएं". 37th Annual Symposium on Foundations of Computer Science: 274–282.
  18. ↑ 18.0 18.1 Ben-Sasson, Eli; Wigderson, Avi (1999). "Short proofs are narrow - resolution made simple". Proceedings of the 31st ACM Symposium on Theory of Computing. pp. 517–526.
  19. ↑ Cook, Stephen (1975). "Feasibly constructive proofs and the propositiona calculus". Proceedings of the 7th Annual ACM Symposium on Theory of Computing. pp. 83–97.
  20. ↑ Paris, Jeff; Wilkie, Alex (1985). "परिबद्ध अंकगणित में समस्याएँ गिनना". Methods in Mathematical Logic. Lecture Notes in Mathematics. 1130: 317–340. doi:10.1007/BFb0075316. ISBN 978-3-540-15236-1.
  21. ↑ Cook, Stephen; Nguyen, Phuong (2010). Logical Foundations of Proof Complexity. Perspectives in Logic. Cambridge: Cambridge University Press. doi:10.1017/CBO9780511676277. ISBN 978-0-521-51729-4. MR 2589550. (draft from 2008)
  22. ↑ Ajtai, M. (1988). "The complexity of the pigeonhole principle". Proceedings of the IEEE 29th Annual Symposium on Foundation of Computer Science. pp. 346–355.
  23. ↑ Haken, A. (1985). "संकल्प की दुरूहता". Theoretical Computer Science. 39: 297–308. doi:10.1016/0304-3975(85)90144-6.
  24. ↑ Ajtai, M. (1988). "The complexity of the pigeonhole principle". Proceedings of the IEEE 29th Annual Symposium on Foundation of Computer Science. pp. 346–355.
  25. ↑ Pitassi, Toniann; Beame, Paul; Impagliazzo, Russell (1993). "पिजनहोल सिद्धांत के लिए घातीय निचली सीमाएँ". Computational Complexity. 3 (2): 97–308. doi:10.1007/BF01200117. S2CID 1046674.
  26. ↑ Krajíček, Jan; Pudlák, Pavel; Woods, Alan (1995). "पिजनहोल सिद्धांत के बाउंडेड डेप्थ फ़्रीज़ प्रूफ़ के आकार के लिए एक घातीय निचला बाउंड". Random Structures and Algorithms. 7 (1): 15–39. doi:10.1002/rsa.3240070103.
  27. ↑ Krajíček, Jan (1994). "स्थिर-गहराई वाले प्रस्ताव प्रमाणों के आकार की निचली सीमाएं". Journal of Symbolic Logic. 59 (1): 73–86. doi:10.2307/2275250. JSTOR 2275250.
  28. ↑ 28.0 28.1 Krajíček, Jan (1997). "अंतर्वेशन प्रमेय, प्रमाण प्रणालियों के लिए निचली सीमाएं, और बंधे हुए अंकगणित के लिए स्वतंत्रता परिणाम". Journal of Symbolic Logic. 62 (2): 69–83. doi:10.2307/2275541. JSTOR 2275541.
  29. ↑ 29.0 29.1 Pudlák, Pavel (1997). "रिज़ॉल्यूशन और कटिंग प्लेन प्रूफ़ और मोनोटोन गणना के लिए निचली सीमाएं". Journal of Symbolic Logic. 62 (3): 981–998. doi:10.2307/2275583. JSTOR 2275583.
  30. ↑ Pudlák, Pavel (2003). "असंयुक्त एनपी-जोड़ों की न्यूनता और समरूपता पर". Theoretical Computer Science. 295: 323–339. doi:10.2307/2275583. JSTOR 2275583.
  31. ↑ Krajíček, Jan; Pudlák, Pavel (1998). "Some consequences of cryptographical conjectures for and EF". Information and Computation. 140 (1): 82–94. doi:10.1006/inco.1997.2674.
  32. ↑ Bonet, M.L.; Pitassi, Toniann; Raz, Ran (2000). "फ्रीज प्रूफ सिस्टम के लिए इंटरपोलेशन और ऑटोमेशन पर". SIAM Journal on Computing. 29 (6): 1939–1967. doi:10.1137/S0097539798353230.
  33. ↑ Bonet, M.L.; Domingo, C.; Gavaldá, R.; Maciel, A.; Pitassi, Toniann (2004). "बाउंडेड-डेप्थ फ़्रीज प्रूफ़ की गैर-स्वचालितता". Computational Complexity. 13 (1–2): 47–68. doi:10.1007/s00037-004-0183-5. S2CID 1360759.
  34. ↑ Hrubeš, Pavel (2007). "मोडल लॉजिक्स के लिए निचली सीमाएं". Journal of Symbolic Logic. 72 (3): 941–958. doi:10.2178/jsl/1191333849. S2CID 1743011.
  35. ↑ Hrubeš, Pavel (2007). "अंतर्ज्ञानवादी तर्क के लिए एक निचली सीमा". Annals of Pure and Applied Logic. 146 (1): 72–90. doi:10.1016/j.apal.2007.01.001.
  36. ↑ Hrubeš, Pavel (2009). "गैर-शास्त्रीय तर्कशास्त्र में प्रमाणों की लंबाई पर". Annals of Pure and Applied Logic. 157 (2–3): 194–205. doi:10.1016/j.apal.2008.09.013.


अग्रिम पठन


बाहरी संबंध

Retrieved from ‘https://www.vigyanwiki.in/index.php?title=प्रूफ_कॉम्पलेक्सिटी&oldid=281302’