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

Latest revision as of 22:25, 2 February 2024

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

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

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

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

प्रूफ सिस्टम्स

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

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

बहुपद आकार के प्रूफ और 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]

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

सैट सॉल्वर

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

लोअर बाउंड

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

हेकेन (1985) ने रिज़ॉल्यूशन और पिजनहोल थ्योरी के लिए एक्सपोनेंशियल लोअर बाउंड प्रूफ को प्रूफ किया था।^[23]
अजताई (1988) ने स्थिर-डेप्थ वाले फ़्रीज सिस्टम और पिजनहोल थ्योरी के लिए सुपरपोलिनोमियल लोअर बाउंड प्रूफ की थी।^[24] इसे क्रेजीसेक, पुडलक और वुड्स और पिटासी, बीम और इम्पाग्लियाज़ो द्वारा^[25] एक्सपोनेंशियल लोअर बाउंड तक दृढ़ किया गया था।^[26] अजताई की लोअर बाउंड यादृच्छिक प्रतिबंधों की विधि का उपयोग करती है, जिसका उपयोग सर्किट कॉम्पलेक्सिटी में 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)$ दोनों को होल्ड करें। इंटरपोलेंट सर्किट केवल $y$ पर विचार करके यह निर्णय लेता है कि या तो $A(x,y)$ अनुचित है अथवा $B(y,z)$ सत्य है। इंटरपोलेंट सर्किट की प्रकृति आरबिटरेरी हो सकती है। तत्पश्चात, $C$ के निर्माण के संकेत के रूप में प्रारंभिक टॉटोलॉजी $A(x,y)\rightarrow B(y,z)$ के प्रूफ का उपयोग करना संभव है। यदि इंटरपोलेंट $C(y)$ , P में टॉटोलॉजी $A(x,y)\rightarrow B(y,z)$ के किसी भी प्रूफ से कुशलता से गणना योग्य है तो प्रूफ सिस्टम P को फैसिबल इंटरपोलेशन कहा जाता है। दक्षता को प्रूफ की लेंथ के संबंध में मापा जाता है: लंबे प्रूफ के लिए इंटरपोलेंट की गणना करना सरल होता है, इसलिए यह गुण प्रूफ सिस्टम की प्रबलता में मोनोटोन-विरोधी प्रतीत होता है।

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

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

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

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

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

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

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

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

यह भी देखें

कम्प्यूटेशनल कॉम्पलेक्सिटी थ्योरी
सर्किट कॉम्पलेक्सिटी
संचार कॉम्पलेक्सिटी
गणितीय लॉजिक
प्रूफ थ्योरी
कॉम्पलेक्सिटी वर्ग
NP (कॉम्पलेक्सिटी)
coNP

संदर्भ

↑ 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.
↑ Pitassi, Toniann; Beame, Paul; Impagliazzo, Russell (1993). "पिजनहोल सिद्धांत के लिए घातीय निचली सीमाएँ". Computational Complexity. 3 (2): 97–308. doi:10.1007/BF01200117. S2CID 1046674.
↑ Krajíček, Jan; Pudlák, Pavel; Woods, Alan (1995). "पिजनहोल सिद्धांत के बाउंडेड डेप्थ फ़्रीज़ प्रूफ़ के आकार के लिए एक घातीय निचला बाउंड". Random Structures and Algorithms. 7 (1): 15–39. doi:10.1002/rsa.3240070103.
↑ 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.

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

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

[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 1: / Line 1: @@
-[[तर्क]] और [[सैद्धांतिक कंप्यूटर विज्ञान]] में, और विशेष रूप से [[प्रमाण सिद्धांत]] और [[कम्प्यूटेशनल जटिलता सिद्धांत]] में, प्रमाण जटिलता वह क्षेत्र है जिसका लक्ष्य उन कम्प्यूटेशनल संसाधनों को समझना और उनका विश्लेषण करना है जो बयानों को साबित करने या खंडन करने के लिए आवश्यक हैं। प्रमाण जटिलता में अनुसंधान मुख्य रूप से विभिन्न प्रस्ताव प्रमाण प्रणालियों में प्रमाण-लंबाई की निचली और ऊपरी सीमा को साबित करने से संबंधित है। उदाहरण के लिए, प्रमाण जटिलता की प्रमुख चुनौतियों में से एक यह दर्शाना है कि फ़्रीज प्रणाली, सामान्य [[प्रस्तावात्मक कलन]], सभी तनातनी के बहुपद-आकार के प्रमाणों को स्वीकार नहीं करती है। यहां प्रमाण का आकार केवल उसमें प्रतीकों की संख्या है, और एक प्रमाण को बहुपद आकार का कहा जाता है यदि यह टॉटोलॉजी के आकार में बहुपद है जो इसे साबित करता है।
+[[तर्क|लॉजिक]] और [[सैद्धांतिक कंप्यूटर विज्ञान|थ्योरेटिकल कंप्यूटर विज्ञान]] में, और विशेष रूप से [[प्रमाण सिद्धांत|प्रूफ थ्योरी]] और [[कम्प्यूटेशनल जटिलता सिद्धांत|कम्प्यूटेशनल कॉम्पलेक्सिटी थ्योरी]] में, '''प्रूफ कॉम्पलेक्सिटी''' वह क्षेत्र है जिसका लक्ष्य उस कम्प्यूटेशनल संसाधनों का अध्ययन और उनका विश्लेषण करना है जो स्टेटमेंट्स को प्रूफ करने अथवा खंडन करने के लिए आवश्यक हैं। प्रूफ कॉम्पलेक्सिटी में अनुसंधान मुख्य रूप से विभिन्न प्रस्ताव प्रूफ सिस्टम्स में प्रूफ-लेंथ की लोअर और अप्पर बाउंड को प्रूफ करने से संबंधित है। उदाहरण के लिए, प्रूफ कॉम्पलेक्सिटी के प्रमुख विचार में से यह दर्शाना है कि फ़्रीज सिस्टम, सामान्य [[प्रस्तावात्मक कलन|प्रोपोज़िशनल कैलकुलस]], सभी टॉटोलॉजीज़ के बहुपद-आकार के प्रूफ को स्वीकार नहीं करता है। यहां प्रूफ का आकार केवल उसमें प्रतीकों की संख्या है, और प्रूफ को बहुपद आकार का कहा जाता है यदि यह टॉटोलॉजी के आकार में बहुपद है जो इसे प्रूफ करता है।
-प्रमाण जटिलता का व्यवस्थित अध्ययन [[स्टीफन कुक]] और [[रॉबर्ट रेकहो]] (1979) के काम से शुरू हुआ, जिन्होंने कम्प्यूटेशनल जटिलता के परिप्रेक्ष्य से एक [[प्रस्ताव प्रमाण प्रणाली]] की मूल परिभाषा प्रदान की। विशेष रूप से कुक और रेकहो ने देखा कि मजबूत और मजबूत प्रपोजल [[फ्रीज प्रणाली]] पर प्रूफ साइज की निचली सीमा साबित करने को [[एन[[पी (जटिलता)]]]] को सीओएनपी से अलग करने की दिशा में एक कदम के रूप में देखा जा सकता है (और इस प्रकार एनपी से पी (जटिलता)), क्योंकि एक प्रपोजल प्रूफ सिस्टम का अस्तित्व जो सभी टॉटोलॉजी के लिए बहुपद आकार के सबूतों को स्वीकार करता है, एनपी = सीओएनपी के बराबर है।
+प्रूफ कॉम्पलेक्सिटी का व्यवस्थित अध्ययन [[स्टीफन कुक]] और [[रॉबर्ट रेकहो]] (1979) के कार्य से प्रारम्भ हुआ, जिन्होंने कम्प्यूटेशनल कॉम्पलेक्सिटी के दृष्टिकोण से [[प्रस्ताव प्रमाण प्रणाली|प्रोपोज़िशनल प्रूफ सिस्टम]] की मूल परिभाषा प्रदान की थी। विशेष रूप से कुक और रेकहो ने देखा कि दृढ़ प्रोपोज़िशनल [[फ्रीज प्रणाली|प्रूफ़ सिस्टम]] पर प्रूफ साइज की लोअर बाउंड प्रूफ करने को [[पी (जटिलता)|NP (कॉम्पलेक्सिटी)]] को coNP से पृथक करने की दिशा में चरण के रूप में देखा जा सकता है (और इस प्रकार NP से P (कॉम्पलेक्सिटी), क्योंकि प्रोपोज़िशनल प्रूफ़ सिस्टम का अस्तित्व है जो बहुपद आकार के प्रूफ को स्वीकार करता है, सभी टॉटोलॉजी के लिए NP=coNP समान है।
-समसामयिक प्रमाण जटिलता अनुसंधान कम्प्यूटेशनल जटिलता, [[कलन विधि]] और गणित के कई क्षेत्रों से विचार और विधियाँ प्राप्त करता है। चूंकि कई महत्वपूर्ण एल्गोरिदम और एल्गोरिदमिक तकनीकों को कुछ प्रूफ सिस्टम के लिए प्रूफ खोज एल्गोरिदम के रूप में डाला जा सकता है, इसलिए इन सिस्टम में प्रूफ आकार पर निचली सीमा साबित करने से संबंधित एल्गोरिदम पर रन-टाइम निचली सीमा का पता चलता है। यह प्रूफ जटिलता को SAT सॉल्वर जैसे अधिक लागू क्षेत्रों से जोड़ता है।
+समसामयिक प्रूफ कॉम्पलेक्सिटी अनुसंधान कम्प्यूटेशनल कॉम्पलेक्सिटी, [[कलन विधि|एल्गोरिदम]] और गणित के कई क्षेत्रों से विचार और विधियाँ प्राप्त करता है। यद्यपि कई महत्वपूर्ण एल्गोरिदम और एल्गोरिदमिक सिस्टम को कुछ प्रूफ सिस्टमों के लिए प्रूफ सर्च एल्गोरिदम के रूप में निक्षेपित किया जा सकता है, इसलिए इन सिस्टम में प्रूफ आकारों पर लोअर सीमाएं प्रूफ करते हैं, इसका अर्थ है कि संबंधित एल्गोरिदम पर रन-टाइम लोअर सीमाएं होती हैं। यह प्रूफ कॉम्पलेक्सिटी को सैट सॉल्वर जैसे अधिक व्यावहारिक क्षेत्रों से संयोजित करता है।
-[[गणितीय तर्क]] प्रस्तावित प्रमाण आकारों का अध्ययन करने के लिए एक रूपरेखा के रूप में भी काम कर सकता है। [[प्रथम-क्रम सिद्धांत]] और, विशेष रूप से, [[पीनो अंकगणित]] के कमजोर टुकड़े, जो बंधे हुए अंकगणित के नाम से आते हैं, प्रस्ताव प्रमाण प्रणालियों के समान संस्करणों के रूप में कार्य करते हैं और व्यवहार्य तर्क के विभिन्न स्तरों के संदर्भ में लघु प्रस्ताव प्रमाणों की व्याख्या के लिए आगे की पृष्ठभूमि प्रदान करते हैं।
+[[गणितीय तर्क|गणितीय लॉजिक]] प्रस्तावित प्रूफ आकारों का अध्ययन करने के लिए फ्रेमवर्क के रूप में भी कार्य कर सकता है। [[प्रथम-क्रम सिद्धांत|प्रथम-क्रम थ्योरी]] और, विशेष रूप से, [[पीनो अंकगणित]] के वीक फ्रेगमेंट, जो सीमित अंकगणित के नाम से आते हैं, प्रस्ताव प्रूफ सिस्टम्स के समान संस्करणों के रूप में कार्य करते हैं और फैसिबल लॉजिक के विभिन्न स्तरों के संदर्भ में लघु प्रस्ताव प्रूफ की व्याख्या के लिए अग्र पृष्ठभूमि प्रदान करते हैं।
-==प्रमाण प्रणालियाँ==
+==प्रूफ सिस्टम्स==
-{{Main|propositional proof system}}
+{{Main|प्रोपोज़िशनल प्रूफ सिस्टम}}
-एक प्रस्तावक प्रमाण प्रणाली को दो इनपुट के साथ प्रमाण-सत्यापन एल्गोरिथ्म P(A,x) के रूप में दिया गया है। यदि P जोड़ी (A,x) को स्वीकार करता है तो हम कहते हैं कि x, A का P-प्रमाण है।
-प्रोपोज़िशनल प्रूफ सिस्टम के उदाहरणों में अनुक्रमिक कैलकुलस, रिज़ॉल्यूशन (तर्क), [[कटिंग-प्लेन विधि]] और फ़्रीज सिस्टम शामिल हैं। [[ज़र्मेलो फ्रेंकेल सेट सिद्धांत]] जैसे मजबूत गणितीय सिद्धांत प्रस्तावात्मक प्रमाण प्रणालियों को भी प्रेरित करते हैं: एक टॉटोलॉजी का प्रमाण <math>\tau</math> ZFC की प्रस्तावात्मक व्याख्या में एक औपचारिक कथन का ZFC-प्रमाण है '<math>\tau</math> एक तनातनी है'.
+प्रोपोज़िशनल प्रूफ सिस्टम को दो इनपुट के साथ प्रूफ-सत्यापन एल्गोरिथ्म P(A,x) के रूप में दिया गया है। यदि P पेयर (A,x) को स्वीकार करता है तो हम कहते हैं कि x, A का P-प्रूफ है। P को बहुपद समय में रन करना आवश्यक है, और इसके अतिरिक्त यह मानना होगा कि A के निकट P-प्रूफ है यदि A टॉटोलॉजी है।
-==बहुपद आकार के प्रमाण और एनपी बनाम सीओएनपी समस्या==
+प्रोपोज़िशनल प्रूफ सिस्टम के उदाहरणों में अनुक्रमिक कैलकुलस, रिज़ॉल्यूशन (लॉजिक), [[कटिंग-प्लेन विधि]] और फ़्रीज सिस्टम सम्मिलित हैं। [[ज़र्मेलो फ्रेंकेल सेट सिद्धांत|ज़र्मेलो फ्रेंकेल सेट थ्योरी]] जैसे दृढ़ गणितीय थ्योरी प्रोपोज़िशनल प्रूफ सिस्टम्स को भी प्रेरित करते हैं: जेडएफसी की प्रोपोज़िशनल व्याख्या में टॉटोलॉजी <math>\tau</math> का प्रूफ औपचारिक कथन '<math>\tau</math> टॉटोलॉजी है' का जेडएफसी-प्रूफ है।
-प्रूफ़ जटिलता आमतौर पर किसी दिए गए टॉटोलॉजी के लिए सिस्टम में संभव प्रूफ़ों के न्यूनतम आकार के संदर्भ में प्रूफ़ प्रणाली की दक्षता को मापती है। एक प्रमाण का आकार (क्रमशः सूत्र) प्रमाण (क्रमशः सूत्र) का प्रतिनिधित्व करने के लिए आवश्यक प्रतीकों की संख्या है। यदि कोई स्थिरांक मौजूद है तो एक प्रस्ताव प्रमाण प्रणाली P बहुपद रूप से परिबद्ध है <math>c</math> ऐसा कि आकार की हर तनातनी <math>n</math> आकार का पी-प्रूफ़ है <math>(n+c)^c</math>. प्रमाण जटिलता का एक केंद्रीय प्रश्न यह समझना है कि क्या टॉटोलॉजी बहुपद-आकार के प्रमाणों को स्वीकार करती है। औपचारिक रूप से,
+==बहुपद आकार के प्रूफ और NP के प्रति coNP प्रॉब्लम==
-<ब्लॉककोट>समस्या (एनपी बनाम सीओएनपी)
+प्रूफ़ कॉम्पलेक्सिटी सामान्यतः किसी दिए गए टॉटोलॉजी के लिए सिस्टम में संभव प्रूफ़ों के न्यूनतम आकार के संदर्भ में प्रूफ़ प्रणाली की दक्षता को मापती है। प्रूफ का आकार (क्रमशः सूत्र) प्रूफ (क्रमशः सूत्र) का प्रतिनिधित्व करने के लिए आवश्यक प्रतीकों की संख्या है। प्रस्ताव प्रूफ सिस्टम P बहुपद रूप से परिबद्ध होती है यदि इसमें स्थिरांक <math>c</math> उपस्थित होता है जैसे कि आकार <math>n</math> के प्रत्येक टॉटोलॉजी में आकार <math>(n+c)^c</math> का P-प्रूफ होता है। प्रूफ कॉम्पलेक्सिटी का केंद्रीय प्रश्न यह समझना है कि क्या टॉटोलॉजी बहुपद-आकार के प्रूफ को स्वीकार करती है। औपचारिक रूप से,
-क्या बहुपद से बंधी प्रस्तावात्मक प्रमाण प्रणाली मौजूद है?
-</ब्लॉककोट>
-कुक और रेकहो (1979) ने देखा कि एक बहुपद रूप से बंधी हुई प्रमाण प्रणाली मौजूद है यदि और केवल यदि NP=coNP। इसलिए, यह साबित करना कि विशिष्ट प्रमाण प्रणालियाँ बहुपद आकार के प्रमाणों को स्वीकार नहीं करती हैं, इसे एनपी और सीओएनपी (और इस प्रकार पी और एनपी) को अलग करने की दिशा में आंशिक प्रगति के रूप में देखा जा सकता है।<ref name="cr">{{cite journal|first1=Stephen|last1=Cook|author-link1=Stephen Cook|first2=Robert A.|last2=Reckhow|title=प्रस्तावक प्रमाण प्रणालियों की सापेक्ष दक्षता|journal=[[Journal of Symbolic Logic]]|volume=44|number=1|year=1979|pages=36–50|doi=10.2307/2273702|jstor=2273702}}</ref>
+'''प्रॉब्लम''' (NP के प्रति coNP)
+क्या बहुपद से परिबद्ध प्रोपोज़िशनल प्रूफ सिस्टम उपस्थित है?
-==प्रमाण प्रणालियों के बीच इष्टतमता और सिमुलेशन==
+कुक और रेकहो (1979) ने देखा कि बहुपद रूप से परिबद्ध प्रूफ सिस्टम उपस्थित है यदि NP=coNP है। इसलिए, यह प्रूफ करना कि विशिष्ट प्रूफ सिस्टम्स बहुपद आकार के प्रूफ को स्वीकार नहीं करते हैं, इसे NP और coNP (और इस प्रकार P और NP) को पृथक करने की दिशा में आंशिक प्रगति के रूप में देखा जा सकता है।<ref name="cr">{{cite journal|first1=Stephen|last1=Cook|author-link1=Stephen Cook|first2=Robert A.|last2=Reckhow|title=प्रस्तावक प्रमाण प्रणालियों की सापेक्ष दक्षता|journal=[[Journal of Symbolic Logic]]|volume=44|number=1|year=1979|pages=36–50|doi=10.2307/2273702|jstor=2273702}}</ref>
-प्रूफ जटिलता सिमुलेशन की धारणा का उपयोग करके प्रूफ सिस्टम की ताकत की तुलना करती है। एक प्रूफ सिस्टम पी पी एक प्रूफ सिस्टम क्यू का अनुकरण करता है यदि कोई बहुपद-समय फ़ंक्शन है जो एक टॉटोलॉजी का क्यू-प्रूफ देता है तो उसी टॉटोलॉजी का एक पी-प्रूफ आउटपुट करता है। यदि पी पी-क्यू का अनुकरण करता है और क्यू पी-पी का अनुकरण करता है, तो प्रमाण प्रणाली पी और क्यू पी-समतुल्य हैं। सिमुलेशन की एक कमजोर धारणा भी है: एक प्रूफ सिस्टम पी एक प्रूफ सिस्टम क्यू का अनुकरण करता है यदि कोई बहुपद पी है जैसे कि टॉटोलॉजी ए के प्रत्येक क्यू-प्रूफ एक्स के लिए, ए का एक पी-प्रूफ वाई है जैसे कि वाई की लंबाई, |y| अधिकतम p(|x|) है।
+== प्रूफ सिस्टम के मध्य ऑप्टिमालिटी और सिमुलेशन ==
+प्रूफ कॉम्पलेक्सिटी सिमुलेशन की धारणा का उपयोग करके प्रूफ सिस्टम के सामर्थ्य की उपमा करती है। प्रूफ सिस्टम 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|) है।
-उदाहरण के लिए, अनुक्रमिक कैलकुलस (प्रत्येक) फ़्रीज प्रणाली के लिए पी-समतुल्य है।<ref name="Rec">{{cite thesis|first1=Robert A.|last1=Reckhow|title=प्रस्तावात्मक गणना में प्रमाणों की लंबाई पर|type=PhD Thesis |publisher=University of Toronto |year=1976}}</ref>
+उदाहरण के लिए, अनुक्रमिक कैलकुलस (प्रत्येक) फ़्रीज सिस्टम के लिए p-समतुल्य है।<ref name="Rec">{{cite thesis|first1=Robert A.|last1=Reckhow|title=प्रस्तावात्मक गणना में प्रमाणों की लंबाई पर|type=PhD Thesis |publisher=University of Toronto |year=1976}}</ref>
-एक प्रूफ सिस्टम पी-इष्टतम है यदि यह अन्य सभी प्रूफ सिस्टमों का पी-अनुकरण करता है, और यह इष्टतम है यदि यह अन्य सभी प्रूफ सिस्टमों का अनुकरण करता है। यह एक खुली समस्या है कि क्या ऐसी प्रमाण प्रणालियाँ मौजूद हैं:
-<ब्लॉककोट>'समस्या' (इष्टतमता)
+प्रूफ सिस्टम p-ऑप्टिमालिटी है यदि यह अन्य सभी प्रूफ सिस्टमों का p-अनुकरण करता है, और यह ऑप्टिमालिटी है यदि यह अन्य सभी प्रूफ सिस्टमों का अनुकरण करता है। यह संवृत प्रॉब्लम है कि क्या ऐसी प्रूफ सिस्टम्स उपस्थित हैं:
-क्या कोई पी-इष्टतम या इष्टतम प्रस्तावक प्रमाण प्रणाली मौजूद है?
-</ब्लॉककोट>
-प्रत्येक प्रस्ताव प्रमाण प्रणाली पी को फ़्रीज प्रणाली # विस्तारित फ़्रीज प्रणाली द्वारा अनुकरण किया जा सकता है जो पी की सुदृढ़ता को अभिगृहीत करने वाले सिद्धांतों के साथ विस्तारित है।<ref name="Kpc">{{cite book|first1=Jan|last1=Krajíček|title=प्रमाण जटिलता|publisher=Cambridge University Press|year=2019}}</ref> एक इष्टतम (क्रमशः पी-इष्टतम) प्रमाण प्रणाली का अस्तित्व इस धारणा से जाना जाता है कि 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>
+'''प्रॉब्लम''' (ऑप्टिमालिटी)
-कई कमजोर प्रूफ प्रणालियों के लिए यह ज्ञात है कि वे कुछ मजबूत प्रणालियों का अनुकरण नहीं करते हैं (नीचे देखें)। हालाँकि, यदि अनुकरण की धारणा को शिथिल कर दिया जाए तो यह प्रश्न खुला रहता है। उदाहरण के लिए, यह खुला है कि क्या रिज़ॉल्यूशन प्रभावी रूप से बहुपद रूप से विस्तारित फ़्रीज का अनुकरण करता है।<ref name="PS">{{cite journal|first1=Toniann|last1=Pitassi|author-link1=Toniann Pitassi|first2=Rahul|last2=Santhanam|author-link2=Rahul Santhanam|title=प्रभावी ढंग से बहुपद सिमुलेशन|url=https://www.cs.toronto.edu/~toni/Papers/effsimulation.pdf|journal=ICS|year=2010|pages=370–382}}</ref>
+क्या कोई 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>
-प्रमाण जटिलता में एक महत्वपूर्ण प्रश्न प्रमाण प्रणालियों में प्रमाण खोजने की जटिलता को समझना है।
+कई वीक प्रूफ सिस्टमों के लिए यह ज्ञात है कि वे कुछ दृढ़ प्रणालियों का अनुकरण नहीं करते हैं (नीचे देखें)। यद्यपि, यदि अनुकरण की धारणा को शिथिल कर दिया जाए तो यह प्रश्न संवृत रहता है। उदाहरण के लिए, यह संवृत है कि क्या रिज़ॉल्यूशन प्रभावी रूप से बहुपद रूप से विस्तारित फ़्रीज का अनुकरण करता है।<ref name="PS">{{cite journal|first1=Toniann|last1=Pitassi|author-link1=Toniann Pitassi|first2=Rahul|last2=Santhanam|author-link2=Rahul Santhanam|title=प्रभावी ढंग से बहुपद सिमुलेशन|url=https://www.cs.toronto.edu/~toni/Papers/effsimulation.pdf|journal=ICS|year=2010|pages=370–382}}</ref>
-<ब्लॉककोट>समस्या (स्वचालितता)
+== प्रूफ सर्च की ऑटोमैटाबिलिटी ==
-क्या रेजोल्यूशन या फ़्रीज सिस्टम जैसे मानक प्रूफ सिस्टम में प्रमाण खोजने के लिए कुशल एल्गोरिदम हैं?
+प्रूफ कॉम्पलेक्सिटी में महत्वपूर्ण प्रश्न प्रूफ सिस्टम्स में प्रूफ सर्च की कॉम्पलेक्सिटी का अध्ययन करना है।
-</ब्लॉककोट>
-प्रश्न को स्वचालितता (जिसे स्वचालितता के रूप में भी जाना जाता है) की धारणा द्वारा औपचारिक रूप दिया जा सकता है।<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>
+'''प्रॉब्लम''' (ऑटोमैटाबिलिटी)
-एक प्रूफ सिस्टम पी स्वचालित है यदि कोई एल्गोरिदम है जो एक टॉटोलॉजी देता है <math>\tau</math> का एक पी-प्रूफ आउटपुट करता है <math>\tau</math> समय में बहुपद के आकार में <math>\tau</math> और सबसे छोटे पी-प्रूफ की लंबाई <math>\tau</math>. ध्यान दें कि यदि कोई प्रमाण प्रणाली बहुपद से बंधी नहीं है, तब भी यह स्वचालित हो सकती है। एक प्रूफ सिस्टम पी कमजोर रूप से स्वचालित है यदि एक प्रूफ सिस्टम आर और एक एल्गोरिदम है जो एक टॉटोलॉजी देता है <math>\tau</math> का एक आर-प्रूफ आउटपुट करता है <math>\tau</math> समय में बहुपद के आकार में <math>\tau</math> और सबसे छोटे पी-प्रूफ की लंबाई <math>\tau</math>.
-माना जाता है कि रुचि की कई प्रमाण प्रणालियाँ गैर-स्वचालित हैं। हालाँकि, वर्तमान में केवल सशर्त नकारात्मक परिणाम ही ज्ञात हैं।
+क्या रेजोल्यूशन अथवा फ़्रीज सिस्टम जैसे मानक प्रूफ सिस्टम में प्रूफ सर्च करने के लिए कुशल एल्गोरिदम हैं?
-* क्रेजीसेक और पुडलक (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>
+प्रश्न को ऑटोमैटाबिलिटी (जिसे ऑटोमैटाबिलिटी के रूप में भी जाना जाता है) की धारणा द्वारा औपचारिक रूप दिया जा सकता है।<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>
-* मारिया लुइसा बोनेट, [[टोनियान पिटासी]] और [[एक बार घाव]] (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>
-* अलेख्नोविच और रज़बोरोव (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>
+प्रूफ सिस्टम P ऑटोमेटिक है यदि कोई एल्गोरिदम है जो टॉटोलॉजी <math>\tau</math> देता है तो <math>\tau</math> के आकार में समय बहुपद में <math>\tau</math> का P-प्रूफ आउटपुट करता है और <math>\tau</math> के सबसे छोटे P-प्रूफ की लेंथ होती है। ध्यान दें कि यदि कोई प्रूफ सिस्टम बहुपद से परिबद्ध नहीं है, तब भी यह ऑटोमेटिक हो सकता है। प्रूफ सिस्टम P अशक्त रूप से ऑटोमेटिक है यदि R प्रूफ सिस्टम और एल्गोरिदम है जिसे टॉटोलॉजी <math>\tau</math> दिया गया है जो <math>\tau</math> के आकार में समय बहुपद में <math>\tau</math> का R-प्रूफ आउटपुट करता है और <math>\tau</math> के सबसे छोटे P-प्रूफ की लेंथ है।
-* एटसेरियस और मुलर (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>
-यह ज्ञात नहीं है कि रिज़ॉल्यूशन की कमजोर स्वचालितता किसी भी मानक जटिलता-सैद्धांतिक कठोरता धारणाओं को तोड़ देगी या नहीं।
+माना जाता है कि ब्याज की कई प्रूफ सिस्टम्स गैर-ऑटोमेटिक हैं। यद्यपि, वर्तमान में केवल प्रतिबंधात्मक ऋणात्मक परिणाम ही ज्ञात हैं।
+* क्रेजीसेक और पुडलक (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>-फ्रेज सिस्टम अशक्त रूप से ऑटोमेटिक नहीं है जब तक कि कुंजी विनिमय अथवा डिफी-हेलमैन योजना 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) ने प्रूफ किया कि ट्री जैसे रिज़ॉल्यूशन और रिज़ॉल्यूशन तब तक ऑटोमेटिक नहीं होते जब तक कि पैरामीटरयुक्त कॉम्पलेक्सिटी 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) द्वारा नलस्टेलेंसैट्ज़ और पॉलीनोमियल कैलकुलस को ऑटोमेटिक करने की 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>\mathsf{NC}^1</math> लॉजिक को औपचारिक बनाने वाले थ्योरी <math>\mathrm {VNC}^1</math> से युग्मित होती है।
-{{Main|Bounded arithmetic}}
-प्रस्तावित प्रमाण प्रणालियों की व्याख्या उच्च क्रम के सिद्धांतों के गैर-समान समकक्षों के रूप में की जा सकती है। समतुल्यता का अध्ययन अक्सर परिबद्ध अंकगणित के सिद्धांतों के संदर्भ में किया जाता है। उदाहरण के लिए, विस्तारित फ्रीज प्रणाली कुक के सिद्धांत से मेल खाती है <math>\mathrm {PV}_1</math> बहुपद-समय तर्क को औपचारिक बनाना और फ़्रीज प्रणाली सिद्धांत से मेल खाती है <math>\mathrm {VNC}^1</math> एनसी (जटिलता) को औपचारिक बनाना#एनसी पदानुक्रम|<math>\mathsf{NC}^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>\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>
+[[जेफ पेरिस (गणितज्ञ)]] और [[एलेक्स विल्की]] (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 78: / 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>
-==सैट सॉल्वर==
-{{See also|SAT solver}}
-टॉटोलॉजी को पहचानने के लिए प्रपोजल प्रूफ सिस्टम की व्याख्या गैर-नियतात्मक एल्गोरिदम के रूप में की जा सकती है। एक प्रमाण प्रणाली पी पर एक सुपरपोलिनोमियल निचली सीमा साबित करना इस प्रकार पी के आधार पर एसएटी के लिए एक बहुपद-समय एल्गोरिदम के अस्तित्व को खारिज कर देता है। उदाहरण के लिए, असंतोषजनक उदाहरणों पर [[डीपीएलएल एल्गोरिदम]] का रन पेड़-जैसे संकल्प खंडन के अनुरूप होता है। इसलिए, पेड़-जैसे रिज़ॉल्यूशन (नीचे देखें) के लिए घातीय निचली सीमाएं SAT के लिए कुशल डीपीएलएल एल्गोरिदम के अस्तित्व को खारिज करती हैं। इसी प्रकार, घातीय रिज़ॉल्यूशन निचली सीमा का अर्थ है कि रिज़ॉल्यूशन पर आधारित SAT सॉल्वर, जैसे कि संघर्ष-संचालित क्लॉज लर्निंग एल्गोरिदम, SAT को कुशलतापूर्वक (सबसे खराब स्थिति में) हल नहीं कर सकते हैं।
-==निचली सीमा==
+जबकि उपर्युक्त पत्राचार कहता है कि थ्योरी में प्रूफ संबंधित प्रूफ सिस्टम में लघु प्रूफ के अनुक्रम में परिवर्तन हो जाता है, तथा विपरीत निहितार्थ का रूप भी प्रस्तावित होता है। सिस्टम 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>
-प्रस्तावित प्रमाणों की लंबाई पर निचली सीमा साबित करना आम तौर पर बहुत मुश्किल होता है। फिर भी, कमजोर प्रूफ सिस्टम के लिए निचली सीमा साबित करने के कई तरीके खोजे गए हैं।
+== सैट सॉल्वर ==
+{{See also|सैट सॉल्वर}}
-* हेकेन (1985) ने रिज़ॉल्यूशन और पिजनहोल सिद्धांत के लिए एक घातीय निचली सीमा साबित की।<ref name="Hak1">{{cite journal|first1=A.|last1=Haken|author-link1=A. Haken|title=संकल्प की दुरूहता|journal=[[Theoretical Computer Science (journal)|Theoretical Computer Science]]|volume=39|year=1985|pages=297–308|doi=10.1016/0304-3975(85)90144-6|doi-access=free}}</ref>
+टॉटोलॉजी को पहचानने के लिए प्रपोजल प्रूफ सिस्टम की व्याख्या अनियतात्मक एल्गोरिदम के रूप में की जा सकती है। प्रूफ सिस्टम P पर सुपरपोलिनोमियल लोअर बाउंड प्रूफ करना इस प्रकार P के आधार पर सैट के लिए बहुपद-समय एल्गोरिदम के अस्तित्व को अस्वीकृत कर देता है। उदाहरण के लिए, असंतोषजनक उदाहरणों पर [[डीपीएलएल एल्गोरिदम]] का रन ट्री-जैसे रिज़ॉल्यूशन खंडन के अनुरूप होता है। इसलिए, ट्री-जैसे रिज़ॉल्यूशन (नीचे देखें) के लिए घातीय लोअर सीमाएं सैट के लिए कुशल डीपीएलएल एल्गोरिदम के अस्तित्व को अस्वीकृत करती हैं। इसी प्रकार, घातीय रिज़ॉल्यूशन लोअर बाउंड का अर्थ है कि रिज़ॉल्यूशन पर आधारित सैट सॉल्वर, जैसे कि कॉनफ्लिक्ट-ड्राइवन क्लॉज लर्निंग एल्गोरिदम, सैट को कुशलतापूर्वक हल नहीं कर सकते हैं।
-* अजताई (1988) ने स्थिर-गहराई वाले फ़्रीज सिस्टम और पिजनहोल सिद्धांत के लिए एक सुपरपोलिनोमियल निचली सीमा साबित की।<ref name="Ajtb">{{cite book|first1=M.|last1=Ajtai|author-link1=M. 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="KPW">{{cite journal|first1=Jan|last1=Krajíček|first2=Pavel|last2=Pudlák|author-link2=Pavel Pudlak|first3=Alan|last3=Woods|author-link3=Alan Woods (mathematician)|title=पिजनहोल सिद्धांत के बाउंडेड डेप्थ फ़्रीज़ प्रूफ़ के आकार के लिए एक घातीय निचला बाउंड|journal=Random Structures and Algorithms|volume=7|number=1|year=1995|pages=15–39|doi=10.1002/rsa.3240070103}}</ref> और पिटासी, बीम और इम्पाग्लियाज़ो द्वारा।<ref name="PBI">{{cite journal|first1=Toniann|last1=Pitassi|author-link1=Toniann Pitassi|first2=Paul|last2=Beame|author-link2=Paul Beame|first3=Russell|last3=Impagliazzo|s2cid=1046674|author-link3=Russell Impagliazzo|title=पिजनहोल सिद्धांत के लिए घातीय निचली सीमाएँ|journal=Computational Complexity|volume=3|year=1993|issue=2|pages=97–308|doi=10.1007/BF01200117}}</ref> अजताई की निचली सीमा यादृच्छिक प्रतिबंधों की विधि का उपयोग करती है, जिसका उपयोग AC0|AC प्राप्त करने के लिए भी किया जाता था<sup>0</sup>[[सर्किट जटिलता]] में निचली सीमाएं।
-* लेस (1994)<ref name="Kr1">{{cite journal|first1=Jan|last1=Krajíček|title=स्थिर-गहराई वाले प्रस्ताव प्रमाणों के आकार की निचली सीमाएं|journal=Journal of Symbolic Logic|volume=59|number=1|year=1994|pages=73–86|doi=10.2307/2275250|jstor=2275250}}</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>
-* पुडलक (1997) ने व्यवहार्य प्रक्षेप के माध्यम से विमानों को काटने के लिए घातीय निचली सीमाएं साबित कीं।<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>
-* बेन-सैसन और विगडरसन (1999) ने रिज़ॉल्यूशन खंडन के आकार की निचली सीमा को कम करके रिज़ॉल्यूशन खंडन की चौड़ाई की निचली सीमा तक एक प्रमाण विधि प्रदान की, जिसने हेकेन की निचली सीमा के कई सामान्यीकरणों को पकड़ लिया।<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>
-फ़्रीज प्रणाली के लिए एक गैर-तुच्छ निचली सीमा प्राप्त करना एक लंबे समय से चली आ रही खुली समस्या है।
-==संभव प्रक्षेप==
+==लोअर बाउंड==
-प्रपत्र की एक तनातनी पर विचार करें <math>A(x,y) \rightarrow B(y,z) </math>. टॉटोलॉजी प्रत्येक विकल्प के लिए सत्य है <math>y</math>, और ठीक करने के बाद <math>y</math> का मूल्यांकन <math>A</math> और <math>B</math> स्वतंत्र हैं क्योंकि वे चरों के असंयुक्त समुच्चयों पर परिभाषित हैं। इसका मतलब यह है कि इंटरपोलेंट सर्किट को परिभाषित करना संभव है <math>C(y)</math>, ऐसे कि दोनों <math>A(x,y) \rightarrow C(y)</math> और <math>C(y) \rightarrow B(y,z)</math> पकड़ना। इंटरपोलेंट सर्किट या तो निर्णय लेता है <math>A(x,y)</math> गलत है या यदि <math>B(y,z)</math> सत्य है, केवल विचार करने से <math>y</math>. इंटरपोलेंट सर्किट की प्रकृति मनमानी हो सकती है। फिर भी, प्रारंभिक टॉटोलॉजी के प्रमाण का उपयोग करना संभव है <math>A(x,y) \rightarrow B(y,z) </math> निर्माण कैसे करें इस पर एक संकेत के रूप में <math>C</math>. कहा जाता है कि एक प्रूफ सिस्टम पी में इंटरपोलेंट होने पर व्यवहार्य इंटरपोलेशन होता है <math>C(y)</math> टॉटोलॉजी के किसी भी प्रमाण से कुशलतापूर्वक गणना की जा सकती है <math>A(x,y) \rightarrow B(y,z)</math> पी में। दक्षता को प्रमाण की लंबाई के संबंध में मापा जाता है: लंबे प्रमाणों के लिए इंटरपोलेंट की गणना करना आसान होता है, इसलिए यह संपत्ति प्रमाण प्रणाली की ताकत में मोनोटोन-विरोधी प्रतीत होती है।
+प्रस्तावित प्रूफ की लेंथ पर लोअर बाउंड प्रूफ करना सामान्यतः कठिन होता है। तत्पश्चात, वीक प्रूफ सिस्टम के लिए लोअर बाउंड प्रूफ करने की कई विधियाँ ज्ञात की गयी हैं।
-निम्नलिखित तीन कथन एक साथ सत्य नहीं हो सकते: (ए) <math>A(x,y) \rightarrow B(y,z)</math> कुछ प्रमाण प्रणाली में एक संक्षिप्त प्रमाण है; (बी) ऐसी प्रमाण प्रणाली में व्यवहार्य प्रक्षेप है; (सी) इंटरपोलेंट सर्किट एक कम्प्यूटेशनल रूप से कठिन समस्या का समाधान करता है। यह स्पष्ट है कि (ए) और (बी) का अर्थ है कि एक छोटा इंटरपोलेंट सर्किट है, जो (सी) के साथ विरोधाभास में है। इस तरह का संबंध गणनाओं पर प्रूफ लंबाई की ऊपरी सीमा को निचली सीमा में बदलने की अनुमति देता है, और कुशल इंटरपोलेशन एल्गोरिदम को प्रूफ लंबाई पर निचली सीमा में बदलने की अनुमति देता है।
+* हेकेन (1985) ने रिज़ॉल्यूशन और पिजनहोल थ्योरी के लिए एक्सपोनेंशियल लोअर बाउंड प्रूफ को प्रूफ किया था।<ref name="Hak1">{{cite journal|first1=A.|last1=Haken|author-link1=A. Haken|title=संकल्प की दुरूहता|journal=[[Theoretical Computer Science (journal)|Theoretical Computer Science]]|volume=39|year=1985|pages=297–308|doi=10.1016/0304-3975(85)90144-6|doi-access=free}}</ref>
+* अजताई (1988) ने स्थिर-डेप्थ वाले फ़्रीज सिस्टम और पिजनहोल थ्योरी के लिए सुपरपोलिनोमियल लोअर बाउंड प्रूफ की थी।<ref name="Ajtb">{{cite book|first1=M.|last1=Ajtai|author-link1=M. 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="PBI">{{cite journal|first1=Toniann|last1=Pitassi|author-link1=Toniann Pitassi|first2=Paul|last2=Beame|author-link2=Paul Beame|first3=Russell|last3=Impagliazzo|s2cid=1046674|author-link3=Russell Impagliazzo|title=पिजनहोल सिद्धांत के लिए घातीय निचली सीमाएँ|journal=Computational Complexity|volume=3|year=1993|issue=2|pages=97–308|doi=10.1007/BF01200117}}</ref> एक्सपोनेंशियल लोअर बाउंड तक दृढ़ किया गया था।<ref name="KPW">{{cite journal|first1=Jan|last1=Krajíček|first2=Pavel|last2=Pudlák|author-link2=Pavel Pudlak|first3=Alan|last3=Woods|author-link3=Alan Woods (mathematician)|title=पिजनहोल सिद्धांत के बाउंडेड डेप्थ फ़्रीज़ प्रूफ़ के आकार के लिए एक घातीय निचला बाउंड|journal=Random Structures and Algorithms|volume=7|number=1|year=1995|pages=15–39|doi=10.1002/rsa.3240070103}}</ref> अजताई की लोअर बाउंड यादृच्छिक प्रतिबंधों की विधि का उपयोग करती है, जिसका उपयोग [[सर्किट जटिलता|सर्किट कॉम्पलेक्सिटी]] में AC<sup>0</sup> लोअर बाउंड प्राप्त करने के लिए भी किया जाता था।
+* क्राजिएक (1994)<ref name="Kr1">{{cite journal|first1=Jan|last1=Krajíček|title=स्थिर-गहराई वाले प्रस्ताव प्रमाणों के आकार की निचली सीमाएं|journal=Journal of Symbolic Logic|volume=59|number=1|year=1994|pages=73–86|doi=10.2307/2275250|jstor=2275250}}</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>
+* पुडलक (1997) ने फैसिबल इंटरपोलेशन के माध्यम से तलों को विभक्त करने के लिए एक्सपोनेंशियल लोअर बाउंड को प्रूफ किया था।<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>
+* बेन-सैसन और विगडरसन (1999) ने रिज़ॉल्यूशन खंडन के आकार की लोअर बाउंड को कम करके रिज़ॉल्यूशन खंडन की विड्थ की लोअर बाउंड तक प्रूफ विधि प्रदान की, जिसने हेकेन की लोअर बाउंड के कई सामान्यीकरणों को कैप्चर कर लिया था।<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>
+फ़्रीज सिस्टम के लिए गैर-तुच्छ लोअर बाउंड प्राप्त करना अधिक समय से चली आ रही संवृत प्रॉब्लम है।
-कुछ प्रूफ सिस्टम जैसे रेजोल्यूशन और कटिंग प्लेन व्यवहार्य प्रक्षेप या इसके वेरिएंट को स्वीकार करते हैं।<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> दूसरी ओर, एक प्रमाण प्रणाली पी की कमजोर स्वचालितता का तात्पर्य है कि पी व्यवहार्य प्रक्षेप को स्वीकार करता है। हालाँकि, यदि कोई प्रूफ सिस्टम पी अपनी स्वयं की सुदृढ़ता को कुशलता से साबित नहीं करता है, तो यह व्यवहार्य प्रक्षेप को स्वीकार करने पर भी कमजोर रूप से स्वचालित नहीं हो सकता है।
-कई गैर-स्वचालितता परिणाम संबंधित प्रणालियों में व्यवहार्य प्रक्षेप के विरुद्ध साक्ष्य प्रदान करते हैं।
+<math>A(x,y) \rightarrow B(y,z) </math> फॉर्म की टॉटोलॉजी पर विचार करें। टॉटोलॉजी <math>y</math> प्रत्येक विकल्प के लिए सत्य है, और <math>y</math> को स्थिर करने के पश्चात <math>A</math> और <math>B</math> का मूल्यांकन स्वतंत्र है क्योंकि उन्हें चर के असंयुक्त सेट पर परिभाषित किया गया है। इसका तात्पर्य यह है कि इंटरपोलेंट सर्किट <math>C(y)</math> को परिभाषित करना संभव है, इस प्रकार <math>A(x,y) \rightarrow C(y)</math> और <math>C(y) \rightarrow B(y,z)</math> दोनों को होल्ड करें। इंटरपोलेंट सर्किट केवल <math>y</math> पर विचार करके यह निर्णय लेता है कि या तो <math>A(x,y)</math> अनुचित है अथवा <math>B(y,z)</math> सत्य है। इंटरपोलेंट सर्किट की प्रकृति आरबिटरेरी हो सकती है। तत्पश्चात, <math>C</math> के निर्माण के संकेत के रूप में प्रारंभिक टॉटोलॉजी <math>A(x,y) \rightarrow B(y,z) </math> के प्रूफ का उपयोग करना संभव है। यदि इंटरपोलेंट <math>C(y)</math>, P में टॉटोलॉजी <math>A(x,y) \rightarrow B(y,z)</math> के किसी भी प्रूफ से कुशलता से गणना योग्य है तो प्रूफ सिस्टम P को फैसिबल इंटरपोलेशन कहा जाता है। दक्षता को प्रूफ की लेंथ के संबंध में मापा जाता है: लंबे प्रूफ के लिए इंटरपोलेंट की गणना करना सरल होता है, इसलिए यह गुण प्रूफ सिस्टम की प्रबलता में मोनोटोन-विरोधी प्रतीत होता है।
-* क्रेजीसेक और पुडलक (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>
+निम्नलिखित तीन स्टेटमेंट्स साथ सत्य नहीं हो सकते: (ए) <math>A(x,y) \rightarrow B(y,z)</math> के निकट कुछ प्रूफ सिस्टम में संक्षिप्त प्रूफ है; (बी) इस प्रकार की प्रूफ सिस्टम में फैसिबल इंटरपोलेशन है; (सी) इंटरपोलेंट सर्किट कम्प्यूटेशनल रूप से समष्टि प्रॉब्लम का समाधान करता है। यह स्पष्ट है कि (ए) और (बी) का अर्थ है कि छोटा इंटरपोलेंट सर्किट है, जो (सी) के साथ विरोधाभास में है। इस प्रकार का संबंध गणनाओं पर प्रूफ लेंथ की अप्पर बाउंड को लोअर बाउंड में परिवर्तित करने की अनुमति देता है, और कुशल इंटरपोलेशन एल्गोरिदम को प्रूफ लेंथ पर लोअर बाउंड में परिवर्तित करने की अनुमति देता है।
-* बोनेट, पिटासी और रज़ (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>
-* बोनेट, डोमिंगो, गवाल्डा, मैकिएल, पिटासी (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>
+कुछ प्रूफ सिस्टम जैसे रेजोल्यूशन और कटिंग प्लेन फैसिबल इंटरपोलेशन या इसके वेरिएंट को स्वीकार करते हैं।<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> मुक्त चर द्वारा एन्कोड किए गए हैं। इसके अतिरिक्त, <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 स्वयं की सुदृढ़ता को कुशलता से प्रूफ नहीं करता है, तो यह फैसिबल इंटरपोलेशन को स्वीकार करने पर भी अशक्त रूप से ऑटोमेटिक नहीं हो सकता है।
-प्रमाणों के आकार की तुलना करने के विचार का उपयोग किसी भी स्वचालित तर्क प्रक्रिया के लिए किया जा सकता है जो प्रमाण उत्पन्न करती है। प्रस्तावात्मक गैर-शास्त्रीय तर्क, विशेष रूप से [[अंतर्ज्ञानवादी तर्क]], [[मोडल तर्क]] और [[गैर-मोनोटोनिक तर्क]] के लिए प्रमाणों के आकार के बारे में कुछ शोध किए गए हैं।
+कई गैर-ऑटोमैटाबिलिटी परिणाम संबंधित प्रणालियों में फैसिबल इंटरपोलेशन के विरुद्ध साक्ष्य प्रदान करते हैं।
-ह्रुबेस (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>
+* क्रेजीसेक और पुडलक (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>
+* बोनेट, डोमिंगो, गवाल्डा, मैकिएल, पिटासी (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>
-*कम्प्यूटेशनल जटिलता सिद्धांत
+== यह भी देखें ==
-*सर्किट जटिलता
+*कम्प्यूटेशनल कॉम्पलेक्सिटी थ्योरी
-*[[संचार जटिलता]]
+*सर्किट कॉम्पलेक्सिटी
-*गणितीय तर्क
+*[[संचार जटिलता|संचार कॉम्पलेक्सिटी]]
-*प्रमाण सिद्धांत
+*गणितीय लॉजिक
-*[[जटिलता वर्ग]]
+*प्रूफ थ्योरी
-*एनपी (जटिलता)
+*[[जटिलता वर्ग|कॉम्पलेक्सिटी वर्ग]]
-*सीओएनपी
+*NP (कॉम्पलेक्सिटी)
+*coNP
 ==संदर्भ==
@@ Line 199: / Line 196: @@
 [[Category: Machine Translated Page]]
 [[Category:Created On 25/07/2023]]
+[[Category:Vigyan Ready]]

Anonymous

Search

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

Namespaces

More

Page actions

Latest revision as of 22:25, 2 February 2024

Contents

प्रूफ सिस्टम्स

बहुपद आकार के प्रूफ और NP के प्रति coNP प्रॉब्लम

प्रूफ सिस्टम के मध्य ऑप्टिमालिटी और सिमुलेशन

प्रूफ सर्च की ऑटोमैटाबिलिटी

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

सैट सॉल्वर

लोअर बाउंड

फैसिबल इंटरपोलेशन

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

यह भी देखें

संदर्भ

अग्रिम पठन

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

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

Latest revision as of 22:25, 2 February 2024

प्रूफ सिस्टम्स

बहुपद आकार के प्रूफ और NP के प्रति coNP प्रॉब्लम

प्रूफ सिस्टम के मध्य ऑप्टिमालिटी और सिमुलेशन

प्रूफ सर्च की ऑटोमैटाबिलिटी

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

सैट सॉल्वर

लोअर बाउंड

फैसिबल इंटरपोलेशन

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

यह भी देखें

संदर्भ

अग्रिम पठन

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories