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

Revision as of 13:32, 6 August 2023

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

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

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

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

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

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

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

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

प्रूफ़ कॉम्पलेक्सिटी सामान्यतः किसी दिए गए टॉटोलॉजी के लिए सिस्टम में संभव प्रूफ़ों के न्यूनतम आकार के संदर्भ में प्रूफ़ प्रणाली की दक्षता को मापती है। प्रमाण का आकार (क्रमशः सूत्र) प्रमाण (क्रमशः सूत्र) का प्रतिनिधित्व करने के लिए आवश्यक प्रतीकों की संख्या है। प्रस्ताव प्रमाण प्रणाली P बहुपद रूप से परिबद्ध होती है यदि इसमें स्थिरांक $c$ उपस्थित होता है जैसे कि आकार $n$ के प्रत्येक टॉटोलॉजी में आकार $(n+c)^{c}$ का 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 स्वचालित है यदि कोई एल्गोरिदम है जो टॉटोलॉजी $\tau$ देता है तो $\tau$ के आकार में समय बहुपद में $\tau$ का P-प्रूफ आउटपुट करता है और $\tau$ के सबसे छोटे P-प्रूफ की लंबाई होती है। ध्यान दें कि यदि कोई प्रूफ सिस्टम बहुपद से परिबद्ध नहीं है, तब भी यह स्वचालित हो सकता है। प्रूफ सिस्टम P अशक्त रूप से स्वचालित है यदि प्रूफ सिस्टम R और एल्गोरिदम है जिसे टॉटोलॉजी $\tau$ दिया गया है जो $\tau$ के आकार में समय बहुपद में $\tau$ का R-प्रूफ आउटपुट करता है और $\tau$ के सबसे छोटे P-प्रूफ की लंबाई है।

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

क्रेजीसेक और पुडलक (1998) ने सिद्ध किया कि एक्सटेंडेड फ्रीज तब तक अशक्त रूप से स्वचालित नहीं है जब तक कि आरएसए एन्क्रिप्शन P/poly के विरुद्ध सुरक्षित न हो।^[7]
मारिया लुइसा बोनेट, टोनियान पिटासी और रेज़ (2000) ने सिद्ध किया कि $TC^{0}$ -फ्रेज सिस्टम अशक्त रूप से स्वचालित नहीं है जब तक कि कुंजी विनिमय अथवा डिफी-हेलमैन योजना 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]

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

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

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

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

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

सैट सॉल्वर

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

निचली सीमा

प्रस्तावित प्रमाणों की लंबाई पर निचली सीमा सिद्ध करना आम तौर पर बहुत मुश्किल होता है। फिर भी, कमजोर प्रूफ सिस्टम के लिए निचली सीमा सिद्ध करने के कई तरीके खोजे गए हैं।

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

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

संभव प्रक्षेप

प्रपत्र की तनातनी पर विचार करें $A(x,y)\rightarrow B(y,z)$ . टॉटोलॉजी प्रत्येक विकल्प के लिए सत्य है $y$ , और ठीक करने के बाद $y$ का मूल्यांकन $A$ और $B$ स्वतंत्र हैं क्योंकि वे चरों के असंयुक्त समुच्चयों पर परिभाषित हैं। इसका मतलब यह है कि इंटरपोलेंट सर्किट को परिभाषित करना संभव है $C(y)$ , ऐसे कि दोनों $A(x,y)\rightarrow C(y)$ और $C(y)\rightarrow B(y,z)$ पकड़ना। इंटरपोलेंट सर्किट या तो निर्णय लेता है $A(x,y)$ गलत है या यदि $B(y,z)$ सत्य है, केवल विचार करने से $y$ . इंटरपोलेंट सर्किट की प्रकृति मनमानी हो सकती है। फिर भी, प्रारंभिक टॉटोलॉजी के प्रमाण का उपयोग करना संभव है $A(x,y)\rightarrow B(y,z)$ निर्माण कैसे करें इस पर संकेत के रूप में $C$ . कहा जाता है कि प्रूफ सिस्टम पी में इंटरपोलेंट होने पर व्यवहार्य इंटरपोलेशन होता है $C(y)$ टॉटोलॉजी के किसी भी प्रमाण से कुशलतापूर्वक गणना की जा सकती है $A(x,y)\rightarrow B(y,z)$ पी में। दक्षता को प्रमाण की लंबाई के संबंध में मापा जाता है: लंबे प्रमाणों के लिए इंटरपोलेंट की गणना करना आसान होता है, इसलिए यह संपत्ति प्रमाण प्रणाली की ताकत में मोनोटोन-विरोधी प्रतीत होती है।

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

कुछ प्रूफ सिस्टम जैसे रेजोल्यूशन और कटिंग प्लेन व्यवहार्य प्रक्षेप या इसके वेरिएंट को स्वीकार करते हैं।^[28]^[29] व्यवहार्य प्रक्षेप को स्वचालितता के कमजोर रूप के रूप में देखा जा सकता है। वास्तव में, कई प्रमाण प्रणालियों के लिए, जैसे कि विस्तारित फ़्रीज, व्यवहार्य प्रक्षेप कमजोर स्वचालितता के बराबर है। विशेष रूप से, कई प्रमाण प्रणालियाँ P अपनी स्वयं की सुदृढ़ता सिद्ध करने में सक्षम हैं, जो तनातनी है $\mathrm {Ref} _{P}(\pi ,\phi ,x)$ यह कहते हुए कि 'यदि $\pi$ सूत्र का पी-प्रूफ है $\phi (x)$ तब $\phi (x)$ धारण'. यहाँ, $\pi ,\phi ,x$ मुक्त चर द्वारा एन्कोड किए गए हैं। इसके अतिरिक्त, पी-प्रूफ़ उत्पन्न करना संभव है $\mathrm {Ref} _{P}(\pi ,\phi ,x)$ बहुपद-समय में की लंबाई दी गई है $\pi$ और $\phi$ . इसलिए, पी की सुदृढ़ता के लघु पी-प्रमाणों से उत्पन्न कुशल इंटरपोलेंट यह तय करेगा कि क्या कोई दिया गया सूत्र है $\phi$ संक्षिप्त पी-प्रूफ़ स्वीकार करता है $\pi$ . इस तरह के इंटरपोलेंट का उपयोग प्रूफ सिस्टम आर को परिभाषित करने के लिए किया जा सकता है जो दर्शाता है कि पी कमजोर रूप से स्वचालित है।^[30] दूसरी ओर, प्रमाण प्रणाली पी की कमजोर स्वचालितता का तात्पर्य है कि पी व्यवहार्य प्रक्षेप को स्वीकार करता है। यद्यपि, यदि कोई प्रूफ सिस्टम पी अपनी स्वयं की सुदृढ़ता को कुशलता से सिद्ध नहीं करता है, तो यह व्यवहार्य प्रक्षेप को स्वीकार करने पर भी कमजोर रूप से स्वचालित नहीं हो सकता है।

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

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

गैर-शास्त्रीय तर्क

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

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

यह भी देखें

कम्प्यूटेशनल कॉम्पलेक्सिटी सिद्धांत
सर्किट कॉम्पलेक्सिटी
संचार कॉम्पलेक्सिटी
गणितीय तर्क
प्रमाण सिद्धांत
कॉम्पलेक्सिटी वर्ग
एनपी (कॉम्पलेक्सिटी)
सीओएनपी

संदर्भ

↑ Cook, Stephen; Reckhow, Robert A. (1979). "प्रस्तावक प्रमाण प्रणालियों की सापेक्ष दक्षता". Journal of Symbolic Logic. 44 (1): 36–50. doi:10.2307/2273702. JSTOR 2273702.
↑ Reckhow, Robert A. (1976). प्रस्तावात्मक गणना में प्रमाणों की लंबाई पर (PhD Thesis). University of Toronto.
↑ Krajíček, Jan (2019). प्रमाण जटिलता. Cambridge University Press.
↑ Krajíček, Jan; Pudlák, Pavel (1989). "प्रस्तावात्मक प्रमाण प्रणालियाँ, प्रथम-क्रम सिद्धांतों की संगति और संगणना की जटिलता". Journal of Symbolic Logic. 54 (3): 1063–1079. doi:10.2307/2274765. JSTOR 2274765.
↑ Pitassi, Toniann; Santhanam, Rahul (2010). "प्रभावी ढंग से बहुपद सिमुलेशन" (PDF). ICS: 370–382.
↑ Bonet, M.L.; Pitassi, Toniann; Raz, Ran (2000). "फ्रीज प्रूफ सिस्टम के लिए इंटरपोलेशन और ऑटोमेशन पर". SIAM Journal on Computing. 29 (6): 1939–1967. doi:10.1137/S0097539798353230.
↑ Krajíček, Jan; Pudlák, Pavel (1998). "Some consequences of cryptographical conjectures for $S_{2}^{1}$ and EF". Information and Computation. 140 (1): 82–94. doi:10.1006/inco.1997.2674.
↑ Bonet, M.L.; Pitassi, Toniann; Raz, Ran (2000). "फ्रीज प्रूफ सिस्टम के लिए इंटरपोलेशन और ऑटोमेशन पर". SIAM Journal on Computing. 29 (6): 1939–1967. doi:10.1137/S0097539798353230.
↑ 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.
↑ 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.
↑ Galesi, Nicola; Lauria, Massimo (2010). "बहुपद कलन की स्वचालितता पर". Theory of Computing Systems. 47 (2): 491–506. doi:10.1007/s00224-009-9195-5. S2CID 11602606.
↑ Mertz, Ian; Pitassi, Toniann; Wei, Yuanhao (2019). "लघु प्रमाण खोजना कठिन है". ICALP.
↑ Atserias, Albert; Müller, Moritz (2019). "Automating resolution is NP-hard". Proceedings of the 60th Symposium on Foundations of Computer Science. pp. 498–509.
↑ de Rezende, Susanna; Göös, Mika; Nordström, Jakob; Pitassi, Tonnian; Robere, Robert; Sokolov, Dmitry (2020). "बीजगणितीय प्रमाण प्रणालियों को स्वचालित करना एनपी-हार्ड है". ECCC.
↑ 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.
↑ Garlík, Michal (2020). "के-डीएनएफ रिज़ॉल्यूशन और इसे स्वचालित करने की एनपी-कठोरता के लिए व्यवहार्य विच्छेदन संपत्ति की विफलता". ECCC. arXiv:2003.10230.
↑ Beame, Paul; Pitassi, Toniann (1996). "सरलीकृत और बेहतर रिज़ॉल्यूशन निचली सीमाएं". 37th Annual Symposium on Foundations of Computer Science: 274–282.
↑ ^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.
↑ Cook, Stephen (1975). "Feasibly constructive proofs and the propositiona calculus". Proceedings of the 7th Annual ACM Symposium on Theory of Computing. pp. 83–97.
↑ 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.
↑ 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)
↑ Ajtai, M. (1988). "The complexity of the pigeonhole principle". Proceedings of the IEEE 29th Annual Symposium on Foundation of Computer Science. pp. 346–355.
↑ Haken, A. (1985). "संकल्प की दुरूहता". Theoretical Computer Science. 39: 297–308. doi:10.1016/0304-3975(85)90144-6.
↑ Ajtai, M. (1988). "The complexity of the pigeonhole principle". Proceedings of the IEEE 29th Annual Symposium on Foundation of Computer Science. pp. 346–355.
↑ Krajíček, Jan; Pudlák, Pavel; Woods, Alan (1995). "पिजनहोल सिद्धांत के बाउंडेड डेप्थ फ़्रीज़ प्रूफ़ के आकार के लिए एक घातीय निचला बाउंड". Random Structures and Algorithms. 7 (1): 15–39. doi:10.1002/rsa.3240070103.
↑ Pitassi, Toniann; Beame, Paul; Impagliazzo, Russell (1993). "पिजनहोल सिद्धांत के लिए घातीय निचली सीमाएँ". Computational Complexity. 3 (2): 97–308. doi:10.1007/BF01200117. S2CID 1046674.
↑ Krajíček, Jan (1994). "स्थिर-गहराई वाले प्रस्ताव प्रमाणों के आकार की निचली सीमाएं". Journal of Symbolic Logic. 59 (1): 73–86. doi:10.2307/2275250. JSTOR 2275250.
↑ ^28.0 ^28.1 Krajíček, Jan (1997). "अंतर्वेशन प्रमेय, प्रमाण प्रणालियों के लिए निचली सीमाएं, और बंधे हुए अंकगणित के लिए स्वतंत्रता परिणाम". Journal of Symbolic Logic. 62 (2): 69–83. doi:10.2307/2275541. JSTOR 2275541.
↑ ^29.0 ^29.1 Pudlák, Pavel (1997). "रिज़ॉल्यूशन और कटिंग प्लेन प्रूफ़ और मोनोटोन गणना के लिए निचली सीमाएं". Journal of Symbolic Logic. 62 (3): 981–998. doi:10.2307/2275583. JSTOR 2275583.
↑ Pudlák, Pavel (2003). "असंयुक्त एनपी-जोड़ों की न्यूनता और समरूपता पर". Theoretical Computer Science. 295: 323–339. doi:10.2307/2275583. JSTOR 2275583.
↑ Krajíček, Jan; Pudlák, Pavel (1998). "Some consequences of cryptographical conjectures for $S_{2}^{1}$ and EF". Information and Computation. 140 (1): 82–94. doi:10.1006/inco.1997.2674.
↑ Bonet, M.L.; Pitassi, Toniann; Raz, Ran (2000). "फ्रीज प्रूफ सिस्टम के लिए इंटरपोलेशन और ऑटोमेशन पर". SIAM Journal on Computing. 29 (6): 1939–1967. doi:10.1137/S0097539798353230.
↑ 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.
↑ Hrubeš, Pavel (2007). "मोडल लॉजिक्स के लिए निचली सीमाएं". Journal of Symbolic Logic. 72 (3): 941–958. doi:10.2178/jsl/1191333849. S2CID 1743011.
↑ Hrubeš, Pavel (2007). "अंतर्ज्ञानवादी तर्क के लिए एक निचली सीमा". Annals of Pure and Applied Logic. 146 (1): 72–90. doi:10.1016/j.apal.2007.01.001.
↑ Hrubeš, Pavel (2009). "गैर-शास्त्रीय तर्कशास्त्र में प्रमाणों की लंबाई पर". Annals of Pure and Applied Logic. 157 (2–3): 194–205. doi:10.1016/j.apal.2008.09.013.

अग्रिम पठन

Beame, Paul; Pitassi, Toniann (1998), "Propositional proof complexity: past, present, and future", Bulletin of the European Association for Theoretical Computer Science, 65: 66–89, MR 1650939, ECCC TR98-067
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)
Krajíček, Jan (1995), Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press
Krajíček, Jan (2005), "Proof complexity" (PDF), in Laptev, A. (ed.), Proceedings of the 4th European Congress of Mathematics, Zürich: European Mathematical Society, pp. 221–231, MR 2185746
Krajíček, Jan, Proof Complexity, Cambridge University Press, 2019.
Pudlák, Pavel (1998), "The lengths of proofs", in Buss, S. R. (ed.), Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics, vol. 137, Amsterdam: North-Holland, pp. 547–637, doi:10.1016/S0049-237X(98)80023-2, MR 1640332

बाहरी संबंध

[cr-1] Cook, Stephen; Reckhow, Robert A. (1979). "प्रस्तावक प्रमाण प्रणालियों की सापेक्ष दक्षता". Journal of Symbolic Logic. 44 (1): 36–50. doi:10.2307/2273702. JSTOR 2273702.

[Rec-2] Reckhow, Robert A. (1976). प्रस्तावात्मक गणना में प्रमाणों की लंबाई पर (PhD Thesis). University of Toronto.

[Kpc-3] Krajíček, Jan (2019). प्रमाण जटिलता. Cambridge University Press.

[KP1-4] Krajíček, Jan; Pudlák, Pavel (1989). "प्रस्तावात्मक प्रमाण प्रणालियाँ, प्रथम-क्रम सिद्धांतों की संगति और संगणना की जटिलता". Journal of Symbolic Logic. 54 (3): 1063–1079. doi:10.2307/2274765. JSTOR 2274765.

[PS-5] Pitassi, Toniann; Santhanam, Rahul (2010). "प्रभावी ढंग से बहुपद सिमुलेशन" (PDF). ICS: 370–382.

[BPR-6] Bonet, M.L.; Pitassi, Toniann; Raz, Ran (2000). "फ्रीज प्रूफ सिस्टम के लिए इंटरपोलेशन और ऑटोमेशन पर". SIAM Journal on Computing. 29 (6): 1939–1967. doi:10.1137/S0097539798353230.

[KP-7] Krajíček, Jan; Pudlák, Pavel (1998). "Some consequences of cryptographical conjectures for $S_{2}^{1}$ and EF". Information and Computation. 140 (1): 82–94. doi:10.1006/inco.1997.2674.

[BPRc-8] Bonet, M.L.; Pitassi, Toniann; Raz, Ran (2000). "फ्रीज प्रूफ सिस्टम के लिए इंटरपोलेशन और ऑटोमेशन पर". SIAM Journal on Computing. 29 (6): 1939–1967. doi:10.1137/S0097539798353230.

[BDGMP-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.

[AleRaz-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.

[GaLa-11] Galesi, Nicola; Lauria, Massimo (2010). "बहुपद कलन की स्वचालितता पर". Theory of Computing Systems. 47 (2): 491–506. doi:10.1007/s00224-009-9195-5. S2CID 11602606.

[MPW-12] Mertz, Ian; Pitassi, Toniann; Wei, Yuanhao (2019). "लघु प्रमाण खोजना कठिन है". ICALP.

[AM-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.

[RGNPRS-14] Rezende, Susanna; Göös, Mika; Nordström, Jakob; Pitassi, Tonnian; Robere, Robert; Sokolov, Dmitry (2020). "बीजगणितीय प्रमाण प्रणालियों को स्वचालित करना एनपी-हार्ड है". ECCC.

[GKMP-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.

[Gar-16] Garlík, Michal (2020). "के-डीएनएफ रिज़ॉल्यूशन और इसे स्वचालित करने की एनपी-कठोरता के लिए व्यवहार्य विच्छेदन संपत्ति की विफलता". ECCC. arXiv:2003.10230.

[BP-17] Beame, Paul; Pitassi, Toniann (1996). "सरलीकृत और बेहतर रिज़ॉल्यूशन निचली सीमाएं". 37th Annual Symposium on Foundations of Computer Science: 274–282.

[BW-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.

[cook-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.

[PW-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.

[CN-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)

[Ajt-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.

[Hak1-23] Haken, A. (1985). "संकल्प की दुरूहता". Theoretical Computer Science. 39: 297–308. doi:10.1016/0304-3975(85)90144-6.

[Ajtb-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.

[KPW-25] Krajíček, Jan; Pudlák, Pavel; Woods, Alan (1995). "पिजनहोल सिद्धांत के बाउंडेड डेप्थ फ़्रीज़ प्रूफ़ के आकार के लिए एक घातीय निचला बाउंड". Random Structures and Algorithms. 7 (1): 15–39. doi:10.1002/rsa.3240070103.

[PBI-26] Pitassi, Toniann; Beame, Paul; Impagliazzo, Russell (1993). "पिजनहोल सिद्धांत के लिए घातीय निचली सीमाएँ". Computational Complexity. 3 (2): 97–308. doi:10.1007/BF01200117. S2CID 1046674.

[Kr1-27] Krajíček, Jan (1994). "स्थिर-गहराई वाले प्रस्ताव प्रमाणों के आकार की निचली सीमाएं". Journal of Symbolic Logic. 59 (1): 73–86. doi:10.2307/2275250. JSTOR 2275250.

[Kr2-28] 28.0 ^28.1 Krajíček, Jan (1997). "अंतर्वेशन प्रमेय, प्रमाण प्रणालियों के लिए निचली सीमाएं, और बंधे हुए अंकगणित के लिए स्वतंत्रता परिणाम". Journal of Symbolic Logic. 62 (2): 69–83. doi:10.2307/2275541. JSTOR 2275541.

[Pu1-29] 29.0 ^29.1 Pudlák, Pavel (1997). "रिज़ॉल्यूशन और कटिंग प्लेन प्रूफ़ और मोनोटोन गणना के लिए निचली सीमाएं". Journal of Symbolic Logic. 62 (3): 981–998. doi:10.2307/2275583. JSTOR 2275583.

[PuNPpairs-30] Pudlák, Pavel (2003). "असंयुक्त एनपी-जोड़ों की न्यूनता और समरूपता पर". Theoretical Computer Science. 295: 323–339. doi:10.2307/2275583. JSTOR 2275583.

[KPb-31] Krajíček, Jan; Pudlák, Pavel (1998). "Some consequences of cryptographical conjectures for $S_{2}^{1}$ and EF". Information and Computation. 140 (1): 82–94. doi:10.1006/inco.1997.2674.

[BPRb-32] Bonet, M.L.; Pitassi, Toniann; Raz, Ran (2000). "फ्रीज प्रूफ सिस्टम के लिए इंटरपोलेशन और ऑटोमेशन पर". SIAM Journal on Computing. 29 (6): 1939–1967. doi:10.1137/S0097539798353230.

[BDGMPb-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.

[Hr1-34] Hrubeš, Pavel (2007). "मोडल लॉजिक्स के लिए निचली सीमाएं". Journal of Symbolic Logic. 72 (3): 941–958. doi:10.2178/jsl/1191333849. S2CID 1743011.

[Hr2-35] Hrubeš, Pavel (2007). "अंतर्ज्ञानवादी तर्क के लिए एक निचली सीमा". Annals of Pure and Applied Logic. 146 (1): 72–90. doi:10.1016/j.apal.2007.01.001.

[Hr3-36] Hrubeš, Pavel (2009). "गैर-शास्त्रीय तर्कशास्त्र में प्रमाणों की लंबाई पर". Annals of Pure and Applied Logic. 157 (2–3): 194–205. doi:10.1016/j.apal.2008.09.013.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29]

[30]

[31]

[32]

[33]

[34]

[35]

[36]

@@ Line 17: / Line 17: @@
 प्रूफ़ कॉम्पलेक्सिटी सामान्यतः किसी दिए गए टॉटोलॉजी के लिए सिस्टम में संभव प्रूफ़ों के न्यूनतम आकार के संदर्भ में प्रूफ़ प्रणाली की दक्षता को मापती है। प्रमाण का आकार (क्रमशः सूत्र) प्रमाण (क्रमशः सूत्र) का प्रतिनिधित्व करने के लिए आवश्यक प्रतीकों की संख्या है। प्रस्ताव प्रमाण प्रणाली P बहुपद रूप से परिबद्ध होती है यदि इसमें स्थिरांक <math>c</math> उपस्थित होता है जैसे कि आकार <math>n</math> के प्रत्येक टॉटोलॉजी में आकार <math>(n+c)^c</math> का P-प्रूफ होता है। प्रूफ कॉम्पलेक्सिटी का केंद्रीय प्रश्न यह समझना है कि क्या टॉटोलॉजी बहुपद-आकार के प्रमाणों को स्वीकार करती है। औपचारिक रूप से,
 '''समस्या''' (NP के प्रति coNP)
@@ Line 31: / Line 30: @@
 प्रूफ सिस्टम p-इष्टतम है यदि यह अन्य सभी प्रूफ सिस्टमों का p-अनुकरण करता है, और यह इष्टतम है यदि यह अन्य सभी प्रूफ सिस्टमों का अनुकरण करता है। यह संवृत समस्या है कि क्या ऐसी प्रमाण प्रणालियाँ उपस्थित हैं:
 '''समस्या''' (इष्टतमता)
 क्या कोई p-इष्टतम या इष्टतम प्रस्तावक प्रमाण प्रणाली उपस्थित है?
 प्रत्येक प्रस्तावित प्रमाण प्रणाली P को P की सुदृढ़ता को अभिगृहीत करने वाले सिद्धांतों के साथ विस्तारित फ़्रीज द्वारा अनुकरण किया जा सकता है।<ref name="Kpc">{{cite book|first1=Jan|last1=Krajíček|title=प्रमाण जटिलता|publisher=Cambridge University Press|year=2019}}</ref> इष्टतम (क्रमशः p-इष्टतम) प्रमाण प्रणाली का अस्तित्व इस धारणा से जाना जाता है कि NE=coNE (क्रमशः E (कॉम्पलेक्सिटी)=NE (कॉम्पलेक्सिटी)) है।<ref name="KP1">{{cite journal|first1=Jan|last1=Krajíček|first2=Pavel|last2=Pudlák|author-link2=Pavel Pudlak|title=प्रस्तावात्मक प्रमाण प्रणालियाँ, प्रथम-क्रम सिद्धांतों की संगति और संगणना की जटिलता|journal=Journal of Symbolic Logic|volume=54|number=3|year=1989|pages=1063–1079|doi=10.2307/2274765|jstor=2274765}}</ref>
@@ Line 44: / Line 41: @@
 == प्रूफ सर्च की स्वचालितता ==
 प्रूफ कॉम्पलेक्सिटी में महत्वपूर्ण प्रश्न प्रमाण प्रणालियों में प्रूफ सर्च की कॉम्पलेक्सिटी का अध्ययन करना है।
 '''समस्या''' (स्वचालितता)
 क्या रेजोल्यूशन अथवा फ़्रीज सिस्टम जैसे मानक प्रूफ सिस्टम में प्रूफ सर्च करने के लिए कुशल एल्गोरिदम हैं?
 प्रश्न को स्वचालितता (जिसे स्वचालितता के रूप में भी जाना जाता है) की धारणा द्वारा औपचारिक रूप दिया जा सकता है।<ref name="BPR">{{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>
@@ Line 57: / Line 52: @@
 माना जाता है कि ब्याज की कई प्रमाण प्रणालियाँ गैर-स्वचालित हैं। यद्यपि, वर्तमान में केवल प्रतिबंधात्मक नकारात्मक परिणाम ही ज्ञात हैं।
-* क्रेजीसेक और पुडलक (1998) ने सिद्ध किया कि ्सटेंडेड फ्रीज तब तक कमजोर रूप से स्वचालित नहीं है जब तक कि [[आरएसए एन्क्रिप्शन]] पी/पॉली के खिलाफ सुरक्षित न हो।<ref name="KP">{{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="KP">{{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>-फ्रेज सिस्टम कमजोर रूप से स्वचालित नहीं है जब तक कि कुंजी ्सचेंज|डिफी-हेलमैन योजना पी/पॉली के खिलाफ सुरक्षित न हो।<ref name="BPRc">{{cite journal|first1=M.L.|last1=Bonet|author-link1=María Luisa 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) द्वारा विस्तारित किया गया था, जिन्होंने सिद्ध किया कि कम से कम 2 गहराई की निरंतर-गहराई वाले फ्रीज सिस्टम तब तक कमजोर रूप से स्वचालित नहीं होते हैं जब तक कि डिफी-हेलमैन योजना उप-घातीय समय में काम करने वाले गैर-समान विरोधियों के खिलाफ सुरक्षित न हो।<ref name="BDGMP">{{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 (journal)|Computational Complexity]]|volume=13|year=2004|issue=1–2|pages=47–68|doi=10.1007/s00037-004-0183-5}}</ref>
+* मारिया लुइसा बोनेट, [[टोनियान पिटासी]] और [[एक बार घाव|रेज़]] (2000) ने सिद्ध किया कि <math>TC^0</math>-फ्रेज सिस्टम अशक्त रूप से स्वचालित नहीं है जब तक कि कुंजी विनिमय अथवा डिफी-हेलमैन योजना P/poly के विरुद्ध सुरक्षित न हो।<ref name="BPRc">{{cite journal|first1=M.L.|last1=Bonet|author-link1=María Luisa 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) द्वारा विस्तारित किया गया था, जिन्होंने सिद्ध किया कि कम से कम 2 गहराई की फ़्रीज़ प्रणालियाँ तब तक अशक्त रूप से स्वचालित नहीं होती हैं जब तक कि डिफी-हेलमैन योजना उप-घातीय समय में कार्य करने वाले असमान विरोधियों के विरुद्ध सुरक्षित न हो।<ref name="BDGMP">{{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 (journal)|Computational Complexity]]|volume=13|year=2004|issue=1–2|pages=47–68|doi=10.1007/s00037-004-0183-5}}</ref>
-* अलेख्नोविच और रज़बोरोव (2008) ने सिद्ध किया कि पेड़ की तरह रिज़ॉल्यूशन और रिज़ॉल्यूशन तब तक स्वचालित नहीं होते जब तक कि पैरामीटरयुक्त कॉम्पलेक्सिटी नहीं होती|एफपीटी=डब्ल्यू[पी]।<ref name="AleRaz">{{cite journal|first1=Michael|last1=Alekhnovich|first2=Alexander|last2=Razborov|title=Resolution is not automatizable unless W[P] is tractable|journal=SIAM Journal on Computing|year=2018|volume=38|issue=4|pages=1347–1363|doi=10.1137/06066850X}}</ref> इसे गैलेसी और लौरिया (2010) द्वारा विस्तारित किया गया था, जिन्होंने सिद्ध किया कि जब तक निश्चित-पैरामीटर पदानुक्रम ध्वस्त नहीं हो जाता, तब तक [[शून्य प्रमेय]] और पॉलीनोमियल कलन स्वचालित नहीं होते हैं।<ref name="GaLa">{{cite journal|first1=Nicola|last1=Galesi|first2=Massimo|last2=Lauria|s2cid=11602606|title=बहुपद कलन की स्वचालितता पर|journal=[[Theory of Computing Systems]]|year=2010|volume=47|issue=2|pages=491–506|doi=10.1007/s00224-009-9195-5}}</ref> मर्ट्ज़, पिटासी और वेई (2019) ने सिद्ध कर दिया कि घातीय समय परिकल्पना को मानते हुए पेड़ जैसे रिज़ॉल्यूशन और रिज़ॉल्यूशन कुछ [[अर्ध-बहुपद समय]] में भी स्वचालित नहीं होते हैं।<ref name="MPW">{{cite journal|first1=Ian|last1=Mertz|first2=Toniann|last2=Pitassi|first3=Yuanhao|last3=Wei|title=लघु प्रमाण खोजना कठिन है|journal=[[ICALP]]|year=2019}}</ref>
+* अलेख्नोविच और रज़बोरोव (2008) ने सिद्ध किया कि ट्री जैसे रिज़ॉल्यूशन और रिज़ॉल्यूशन तब तक स्वचालित नहीं होते जब तक कि पैरामीटरयुक्त कॉम्पलेक्सिटी FPT=W[P] न हो।<ref name="AleRaz">{{cite journal|first1=Michael|last1=Alekhnovich|first2=Alexander|last2=Razborov|title=Resolution is not automatizable unless W[P] is tractable|journal=SIAM Journal on Computing|year=2018|volume=38|issue=4|pages=1347–1363|doi=10.1137/06066850X}}</ref> इसे गैलेसी और लौरिया (2010) द्वारा विस्तारित किया गया था, जिन्होंने सिद्ध किया कि जब तक निश्चित-पैरामीटर पदानुक्रम ध्वस्त नहीं हो जाता, तब तक [[शून्य प्रमेय]] और पॉलीनोमियल कलन स्वचालित नहीं होते हैं।<ref name="GaLa">{{cite journal|first1=Nicola|last1=Galesi|first2=Massimo|last2=Lauria|s2cid=11602606|title=बहुपद कलन की स्वचालितता पर|journal=[[Theory of Computing Systems]]|year=2010|volume=47|issue=2|pages=491–506|doi=10.1007/s00224-009-9195-5}}</ref> मर्ट्ज़, पिटासी और वेई (2019) ने सिद्ध कर दिया कि घातीय समय परिकल्पना को मानते हुए ट्री जैसे रिज़ॉल्यूशन और रिज़ॉल्यूशन कुछ [[अर्ध-बहुपद समय]] में भी स्वचालित नहीं होते हैं।<ref name="MPW">{{cite journal|first1=Ian|last1=Mertz|first2=Toniann|last2=Pitassi|first3=Yuanhao|last3=Wei|title=लघु प्रमाण खोजना कठिन है|journal=[[ICALP]]|year=2019}}</ref>
-* एटसेरियस और मुलर (2019) ने सिद्ध कर दिया कि रिज़ॉल्यूशन तब तक स्वचालित नहीं है जब तक कि P=NP न हो।<ref name="AM">{{cite book|first1=Albert|last1=Atserias|author-link1=Albert Atserias|first2=Moritz|last2=Müller|chapter=Automating resolution is NP-hard|title=Proceedings of the 60th Symposium on Foundations of Computer Science|year=2019|pages=498–509}}</ref> इसे डी रेज़ेंडे, गूस, नॉर्डस्ट्रॉम, पिटासी, रोबेरे और सोकोलोव (2020) द्वारा नलस्टेलेंसैट्ज़ और पॉलीनोमियल कलन को स्वचालित करने की एनपी-कठोरता तक बढ़ाया गया था;<ref name="RGNPRS">{{cite journal|first1=Susanna|last1=de Rezende|first2=Mika|last2=Göös|first3=Jakob|last3=Nordström|first4=Tonnian|last4=Pitassi|first5=Robert|last5=Robere|first6=Dmitry|last6=Sokolov|title=बीजगणितीय प्रमाण प्रणालियों को स्वचालित करना एनपी-हार्ड है|journal=[[Electronic Colloquium on Computational Complexity|ECCC]]|year=2020}}</ref> गोओस, कोरोथ, मर्ट्ज़ और पिटासी (2020) द्वारा कटिंग विमानों को स्वचालित करने की एनपी-कठोरता;<ref name="GKMP">{{cite journal|first1=Mika|last1=Göös|first2=Sajin|last2=Koroth|first3=Ian|last3=Mertz|first4=Tonnian|last4=Pitassi|s2cid=215814356|title=कटिंग विमानों को स्वचालित करना एनपी-हार्ड है|journal=[[Symposium on Theory of Computing|STOC]]|year=2020|pages=68–77|doi=10.1145/3357713.3384248|arxiv=2004.08037|isbn=9781450369794}}</ref> और गार्लिक (2020) द्वारा के-डिसजंक्टिव सामान्य फॉर्म रिज़ॉल्यूशन को स्वचालित करने की एनपी-कठोरता।<ref name="Gar">{{cite journal|first1=Michal|last1=Garlík|title=''के''-डीएनएफ रिज़ॉल्यूशन और इसे स्वचालित करने की एनपी-कठोरता के लिए व्यवहार्य विच्छेदन संपत्ति की विफलता|journal=[[Electronic Colloquium on Computational Complexity|ECCC]]|year=2020|arxiv=2003.10230}}</ref>
+* एटसेरियस और मुलर (2019) ने सिद्ध कर दिया कि रिज़ॉल्यूशन तब तक स्वचालित नहीं है जब तक कि P=NP न हो।<ref name="AM">{{cite book|first1=Albert|last1=Atserias|author-link1=Albert Atserias|first2=Moritz|last2=Müller|chapter=Automating resolution is NP-hard|title=Proceedings of the 60th Symposium on Foundations of Computer Science|year=2019|pages=498–509}}</ref> इसे डी रेज़ेंडे, गूस, नॉर्डस्ट्रॉम, पिटासी, रोबेरे और सोकोलोव (2020) द्वारा नलस्टेलेंसैट्ज़ और पॉलीनोमियल कलन को स्वचालित करने की NP-कठोरता तक विस्तारित किया गया था;<ref name="RGNPRS">{{cite journal|first1=Susanna|last1=de Rezende|first2=Mika|last2=Göös|first3=Jakob|last3=Nordström|first4=Tonnian|last4=Pitassi|first5=Robert|last5=Robere|first6=Dmitry|last6=Sokolov|title=बीजगणितीय प्रमाण प्रणालियों को स्वचालित करना एनपी-हार्ड है|journal=[[Electronic Colloquium on Computational Complexity|ECCC]]|year=2020}}</ref> इसे गोओस, कोरोथ, मर्ट्ज़ और पिटासी (2020) द्वारा कटिंग प्लेनों को स्वचालित करने की NP-कठोरता तक विस्तारित किया गया था;<ref name="GKMP">{{cite journal|first1=Mika|last1=Göös|first2=Sajin|last2=Koroth|first3=Ian|last3=Mertz|first4=Tonnian|last4=Pitassi|s2cid=215814356|title=कटिंग विमानों को स्वचालित करना एनपी-हार्ड है|journal=[[Symposium on Theory of Computing|STOC]]|year=2020|pages=68–77|doi=10.1145/3357713.3384248|arxiv=2004.08037|isbn=9781450369794}}</ref> तथा गार्लिक (2020) द्वारा के-डिसजंक्टिव सामान्य फॉर्म रिज़ॉल्यूशन को स्वचालित करने की NP-कठोरता तक भी विस्तारित किया गया था।<ref name="Gar">{{cite journal|first1=Michal|last1=Garlík|title=''के''-डीएनएफ रिज़ॉल्यूशन और इसे स्वचालित करने की एनपी-कठोरता के लिए व्यवहार्य विच्छेदन संपत्ति की विफलता|journal=[[Electronic Colloquium on Computational Complexity|ECCC]]|year=2020|arxiv=2003.10230}}</ref>
-यह ज्ञात नहीं है कि रिज़ॉल्यूशन की कमजोर स्वचालितता किसी भी मानक कॉम्पलेक्सिटी-सैद्धांतिक कठोरता धारणाओं को तोड़ देगी या नहीं।
+यह ज्ञात नहीं है कि रिज़ॉल्यूशन की अशक्त स्वचालितता किसी भी मानक कॉम्पलेक्सिटी-सैद्धांतिक कठोरता की धारणाओं को खंडित करेगी या नहीं करेगी।
 सकारात्मक पक्ष पर,
-* बीम और पिटासी (1996) ने दिखाया कि पेड़ जैसा रिज़ॉल्यूशन अर्ध-बहुपद समय में स्वचालित होता है और रिज़ॉल्यूशन कमजोर उप-घातीय समय में छोटी चौड़ाई के सूत्रों पर स्वचालित होता है।<ref name="BP">{{cite journal|first1=Paul|last1=Beame|author-link1=Paul Beame|first2=Toniann|last2=Pitassi|author-link2=Toniann Pitassi|title=सरलीकृत और बेहतर रिज़ॉल्यूशन निचली सीमाएं|journal=37th Annual Symposium on Foundations of Computer Science|year=1996|pages=274–282}}</ref><ref name="BW">{{cite book|first1=Eli|last1=Ben-Sasson|author-link1=Eli Ben-Sasson|first2=Avi|last2=Wigderson|author-link2=Avi Wigderson|chapter=Short proofs are narrow - resolution made simple|title=Proceedings of the 31st ACM Symposium on Theory of Computing|year=1999|pages=517–526}}</ref>
+* बीम और पिटासी (1996) ने दर्शाया कि ट्री जैसा रिज़ॉल्यूशन अर्ध-बहुपद समय में स्वचालित होता है और रिज़ॉल्यूशन अशक्त उप-घातीय समय में स्माल विड्थ के सूत्रों पर स्वचालित होता है।<ref name="BP">{{cite journal|first1=Paul|last1=Beame|author-link1=Paul Beame|first2=Toniann|last2=Pitassi|author-link2=Toniann Pitassi|title=सरलीकृत और बेहतर रिज़ॉल्यूशन निचली सीमाएं|journal=37th Annual Symposium on Foundations of Computer Science|year=1996|pages=274–282}}</ref><ref name="BW">{{cite book|first1=Eli|last1=Ben-Sasson|author-link1=Eli Ben-Sasson|first2=Avi|last2=Wigderson|author-link2=Avi Wigderson|chapter=Short proofs are narrow - resolution made simple|title=Proceedings of the 31st ACM Symposium on Theory of Computing|year=1999|pages=517–526}}</ref>
 == परिबद्ध अंकगणित ==
 {{Main|परिबद्ध अंकगणित}}
-प्रस्तावित प्रमाण प्रणालियों की व्याख्या उच्च क्रम के सिद्धांतों के गैर-समान समकक्षों के रूप में की जा सकती है। समतुल्यता का अध्ययन अक्सर परिबद्ध अंकगणित के सिद्धांतों के संदर्भ में किया जाता है। उदाहरण के लिए, विस्तारित फ्रीज प्रणाली कुक के सिद्धांत से मेल खाती है <math>\mathrm {PV}_1</math> बहुपद-समय तर्क को औपचारिक बनाना और फ़्रीज सिस्टम सिद्धांत से मेल खाती है <math>\mathrm {VNC}^1</math> एनसी (कॉम्पलेक्सिटी) को औपचारिक बनाना#एनसी पदानुक्रम|<math>\mathsf{NC}^1</math>विचार।
+प्रस्तावित प्रमाण प्रणालियों की व्याख्या उच्च क्रम के सिद्धांतों के असमान समकक्षों के रूप में की जा सकती है। समतुल्यता का अध्ययन अधिकांशतः परिबद्ध अंकगणित के सिद्धांतों के संदर्भ में किया जाता है। उदाहरण के लिए, विस्तारित फ़्रीज प्रणाली कुक के सिद्धांत <math>\mathrm {PV}_1</math> से युग्मित होती है जो बहुपद-समय तर्क को औपचारिक बनाती है और फ़्रीज प्रणाली <math>\mathsf{NC}^1</math> तर्क को औपचारिक बनाने वाले सिद्धांत <math>\mathrm {VNC}^1</math> से युग्मित होती है।
-पत्राचार स्टीफन कुक (1975) द्वारा प्रस्तुत किया गया था, जिन्होंने औपचारिक रूप से उस सीओएनपी प्रमेय को दिखाया था <math>\Pi^b_1</math> सूत्र, सिद्धांत के <math>\mathrm {PV}_1</math> विस्तारित फ़्रीज में बहुपद-आकार के प्रमाणों के साथ टॉटोलॉजी के अनुक्रमों का अनुवाद करें। इसके अलावा, ्सटेंडेड फ्रीज ऐसी सबसे कमजोर प्रणाली है: यदि किसी अन्य प्रूफ सिस्टम पी में यह संपत्ति है, तो पी ्सटेंडेड फ्रीज का अनुकरण करता है।<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>
-[[जेफ पेरिस (गणितज्ञ)]] और [[एलेक्स विल्की]] (1985) द्वारा दिए गए दूसरे क्रम के तर्क | दूसरे क्रम के बयानों और प्रस्ताव सूत्रों के मध्य वैकल्पिक अनुवाद विस्तारित फ्रीज जैसे फ्रीज या निरंतर-गहराई फ्रीज के उप-प्रणालियों को कैप्चर करने के लिए अधिक व्यावहारिक रहा है।<ref name="PW">{{cite journal|first1=Jeff|last1=Paris|author-link1=Jeff Paris (mathematician)|first2=Alex|last2=Wilkie|author-link2=Alex Wilkie|title=परिबद्ध अंकगणित में समस्याएँ गिनना|journal=Methods in Mathematical Logic|series=Lecture Notes in Mathematics|volume=1130|year=1985|pages=317–340|doi=10.1007/BFb0075316|isbn=978-3-540-15236-1}}</ref><ref name="CN">{{cite book|last1 = Cook | first1 = Stephen | author1-link = Stephen Cook
+[[जेफ पेरिस (गणितज्ञ)]] और [[एलेक्स विल्की]] (1985) द्वारा दिए गए द्वितीय क्रम के स्टेटमेंट्स और प्रस्तावित सूत्रों के मध्य वैकल्पिक अनुवाद एक्सटेंडेड फ्रीज जैसे फ्रीज अथवा निरंतर-डेप्थ फ्रीज के सबसिस्टम्स को कैप्चर करने के लिए अधिक व्यावहारिक रहा है।<ref name="PW">{{cite journal|first1=Jeff|last1=Paris|author-link1=Jeff Paris (mathematician)|first2=Alex|last2=Wilkie|author-link2=Alex Wilkie|title=परिबद्ध अंकगणित में समस्याएँ गिनना|journal=Methods in Mathematical Logic|series=Lecture Notes in Mathematics|volume=1130|year=1985|pages=317–340|doi=10.1007/BFb0075316|isbn=978-3-540-15236-1}}</ref><ref name="CN">{{cite book|last1 = Cook | first1 = Stephen | author1-link = Stephen Cook
   | last2 = Nguyen | first2 = Phuong| doi = 10.1017/CBO9780511676277
   | isbn = 978-0-521-51729-4
@@ Line 82: / Line 78: @@
   | title = Logical Foundations of Proof Complexity
   | year = 2010}} ([http://www.cs.toronto.edu/~sacook/homepage/book draft from 2008])</ref>
-जबकि उपर्युक्त पत्राचार कहता है कि सिद्धांत में प्रमाण संबंधित प्रमाण प्रणाली में लघु प्रमाणों के अनुक्रम में तब्दील हो जाते हैं, विपरीत निहितार्थ का रूप भी लागू होता है। सिस्टम पी के अनुरूप सिद्धांत टी के उपयुक्त [[मॉडल (तर्क)]] का निर्माण करके प्रमाण प्रणाली पी में प्रमाण के आकार पर निचली सीमा प्राप्त करना संभव है। यह [[मॉडल-सैद्धांतिक]] निर्माणों के माध्यम से कॉम्पलेक्सिटी की निचली सीमा को सिद्ध करने की अनुमति देता है, दृष्टिकोण जिसे मिक्लोस अजताई की विधि के रूप में जाना जाता है।<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>
+जबकि उपर्युक्त पत्राचार कहता है कि सिद्धांत में प्रमाण संबंधित प्रमाण प्रणाली में लघु प्रमाणों के अनुक्रम में परिवर्तित हो जाते हैं, विपरीत निहितार्थ का रूप भी लागू होता है। सिस्टम पी के अनुरूप सिद्धांत टी के उपयुक्त [[मॉडल (तर्क)]] का निर्माण करके प्रमाण प्रणाली पी में प्रमाण के आकार पर निचली सीमा प्राप्त करना संभव है। यह [[मॉडल-सैद्धांतिक]] निर्माणों के माध्यम से कॉम्पलेक्सिटी की निचली सीमा को सिद्ध करने की अनुमति देता है, दृष्टिकोण जिसे मिक्लोस अजताई की विधि के रूप में जाना जाता है।<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>
 == सैट सॉल्वर ==
-{{See also|SAT solver}}
+{{See also|सैट सॉल्वर}}
 टॉटोलॉजी को पहचानने के लिए प्रपोजल प्रूफ सिस्टम की व्याख्या गैर-नियतात्मक एल्गोरिदम के रूप में की जा सकती है। प्रमाण प्रणाली पी पर सुपरपोलिनोमियल निचली सीमा सिद्ध करना इस प्रकार पी के आधार पर एसएटी के लिए बहुपद-समय एल्गोरिदम के अस्तित्व को खारिज कर देता है। उदाहरण के लिए, असंतोषजनक उदाहरणों पर [[डीपीएलएल एल्गोरिदम]] का रन पेड़-जैसे संकल्प खंडन के अनुरूप होता है। इसलिए, पेड़-जैसे रिज़ॉल्यूशन (नीचे देखें) के लिए घातीय निचली सीमाएं SAT के लिए कुशल डीपीएलएल एल्गोरिदम के अस्तित्व को खारिज करती हैं। इसी प्रकार, घातीय रिज़ॉल्यूशन निचली सीमा का अर्थ है कि रिज़ॉल्यूशन पर आधारित SAT सॉल्वर, जैसे कि संघर्ष-संचालित क्लॉज लर्निंग एल्गोरिदम, SAT को कुशलतापूर्वक (सबसे खराब स्थिति में) हल नहीं कर सकते हैं।
@@ Line 107: / Line 104: @@
 कुछ प्रूफ सिस्टम जैसे रेजोल्यूशन और कटिंग प्लेन व्यवहार्य प्रक्षेप या इसके वेरिएंट को स्वीकार करते हैं।<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> तब <math>\phi(x)</math> धारण'. यहाँ, <math>\pi,\phi,x</math> मुक्त चर द्वारा एन्कोड किए गए हैं। इसके अलावा, पी-प्रूफ़ उत्पन्न करना संभव है <math>\mathrm{Ref}_P(\pi,\phi,x)</math> बहुपद-समय में की लंबाई दी गई है <math>\pi</math> और <math>\phi</math>. इसलिए, पी की सुदृढ़ता के लघु पी-प्रमाणों से उत्पन्न कुशल इंटरपोलेंट यह तय करेगा कि क्या कोई दिया गया सूत्र है <math>\phi</math> संक्षिप्त पी-प्रूफ़ स्वीकार करता है <math>\pi</math>. इस तरह के इंटरपोलेंट का उपयोग प्रूफ सिस्टम आर को परिभाषित करने के लिए किया जा सकता है जो दर्शाता है कि पी कमजोर रूप से स्वचालित है।<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> तब <math>\phi(x)</math> धारण'. यहाँ, <math>\pi,\phi,x</math> मुक्त चर द्वारा एन्कोड किए गए हैं। इसके अतिरिक्त, पी-प्रूफ़ उत्पन्न करना संभव है <math>\mathrm{Ref}_P(\pi,\phi,x)</math> बहुपद-समय में की लंबाई दी गई है <math>\pi</math> और <math>\phi</math>. इसलिए, पी की सुदृढ़ता के लघु पी-प्रमाणों से उत्पन्न कुशल इंटरपोलेंट यह तय करेगा कि क्या कोई दिया गया सूत्र है <math>\phi</math> संक्षिप्त पी-प्रूफ़ स्वीकार करता है <math>\pi</math>. इस तरह के इंटरपोलेंट का उपयोग प्रूफ सिस्टम आर को परिभाषित करने के लिए किया जा सकता है जो दर्शाता है कि पी कमजोर रूप से स्वचालित है।<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> दूसरी ओर, प्रमाण प्रणाली पी की कमजोर स्वचालितता का तात्पर्य है कि पी व्यवहार्य प्रक्षेप को स्वीकार करता है। यद्यपि, यदि कोई प्रूफ सिस्टम पी अपनी स्वयं की सुदृढ़ता को कुशलता से सिद्ध नहीं करता है, तो यह व्यवहार्य प्रक्षेप को स्वीकार करने पर भी कमजोर रूप से स्वचालित नहीं हो सकता है।
 कई गैर-स्वचालितता परिणाम संबंधित प्रणालियों में व्यवहार्य प्रक्षेप के विरुद्ध साक्ष्य प्रदान करते हैं।
-* क्रेजीसेक और पुडलक (1998) ने सिद्ध किया कि ्सटेंडेड फ्रीज तब तक व्यवहार्य इंटरपोलेशन को स्वीकार नहीं करता जब तक कि आरएसए पी/पॉली के खिलाफ सुरक्षित न हो।<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>-फ्रेज सिस्टम तब तक व्यवहार्य प्रक्षेप को स्वीकार नहीं करता जब तक कि डिफी-हेलमैन योजना पी/पॉली के खिलाफ सुरक्षित न हो।<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>
 == यह भी देखें ==