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

Revision as of 23:50, 4 August 2023

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

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

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

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

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

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

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

बहुपद आकार के प्रमाण और एनपी बनाम सीओएनपी समस्या

प्रूफ़ जटिलता आमतौर पर किसी दिए गए टॉटोलॉजी के लिए सिस्टम में संभव प्रूफ़ों के न्यूनतम आकार के संदर्भ में प्रूफ़ प्रणाली की दक्षता को मापती है। प्रमाण का आकार (क्रमशः सूत्र) प्रमाण (क्रमशः सूत्र) का प्रतिनिधित्व करने के लिए आवश्यक प्रतीकों की संख्या है। यदि कोई स्थिरांक मौजूद है तो प्रस्ताव प्रमाण प्रणाली P बहुपद रूप से परिबद्ध है $c$ ऐसा कि आकार की हर तनातनी $n$ आकार का पी-प्रूफ़ है $(n+c)^{c}$ . प्रमाण जटिलता का केंद्रीय प्रश्न यह समझना है कि क्या टॉटोलॉजी बहुपद-आकार के प्रमाणों को स्वीकार करती है। औपचारिक रूप से,

<ब्लॉककोट>समस्या (एनपी बनाम सीओएनपी) क्या बहुपद से बंधी प्रस्तावात्मक प्रमाण प्रणाली मौजूद है? </ब्लॉककोट>

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

प्रमाण प्रणालियों के बीच इष्टतमता और सिमुलेशन

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

उदाहरण के लिए, अनुक्रमिक कैलकुलस (प्रत्येक) फ़्रीज प्रणाली के लिए पी-समतुल्य है।^[2] प्रूफ सिस्टम पी-इष्टतम है यदि यह अन्य सभी प्रूफ सिस्टमों का पी-अनुकरण करता है, और यह इष्टतम है यदि यह अन्य सभी प्रूफ सिस्टमों का अनुकरण करता है। यह खुली समस्या है कि क्या ऐसी प्रमाण प्रणालियाँ मौजूद हैं:

<ब्लॉककोट>'समस्या' (इष्टतमता) क्या कोई पी-इष्टतम या इष्टतम प्रस्तावक प्रमाण प्रणाली मौजूद है? </ब्लॉककोट>

प्रत्येक प्रस्ताव प्रमाण प्रणाली पी को फ़्रीज प्रणाली # विस्तारित फ़्रीज प्रणाली द्वारा अनुकरण किया जा सकता है जो पी की सुदृढ़ता को अभिगृहीत करने वाले सिद्धांतों के साथ विस्तारित है।^[3] इष्टतम (क्रमशः पी-इष्टतम) प्रमाण प्रणाली का अस्तित्व इस धारणा से जाना जाता है कि NE=coNE (क्रमशः E (जटिलता)=NE (जटिलता))।^[4] कई कमजोर प्रूफ प्रणालियों के लिए यह ज्ञात है कि वे कुछ मजबूत प्रणालियों का अनुकरण नहीं करते हैं (नीचे देखें)। हालाँकि, यदि अनुकरण की धारणा को शिथिल कर दिया जाए तो यह प्रश्न खुला रहता है। उदाहरण के लिए, यह खुला है कि क्या रिज़ॉल्यूशन प्रभावी रूप से बहुपद रूप से विस्तारित फ़्रीज का अनुकरण करता है।^[5]

प्रमाण खोज की स्वचालितता

प्रमाण जटिलता में महत्वपूर्ण प्रश्न प्रमाण प्रणालियों में प्रमाण खोजने की जटिलता को समझना है।

<ब्लॉककोट>समस्या (स्वचालितता) क्या रेजोल्यूशन या फ़्रीज सिस्टम जैसे मानक प्रूफ सिस्टम में प्रमाण खोजने के लिए कुशल एल्गोरिदम हैं? </ब्लॉककोट>

प्रश्न को स्वचालितता (जिसे स्वचालितता के रूप में भी जाना जाता है) की धारणा द्वारा औपचारिक रूप दिया जा सकता है।^[6] प्रूफ सिस्टम पी स्वचालित है यदि कोई एल्गोरिदम है जो टॉटोलॉजी देता है $\tau$ का पी-प्रूफ आउटपुट करता है $\tau$ समय में बहुपद के आकार में $\tau$ और सबसे छोटे पी-प्रूफ की लंबाई $\tau$ . ध्यान दें कि यदि कोई प्रमाण प्रणाली बहुपद से बंधी नहीं है, तब भी यह स्वचालित हो सकती है। प्रूफ सिस्टम पी कमजोर रूप से स्वचालित है यदि प्रूफ सिस्टम आर और एल्गोरिदम है जो टॉटोलॉजी देता है $\tau$ का आर-प्रूफ आउटपुट करता है $\tau$ समय में बहुपद के आकार में $\tau$ और सबसे छोटे पी-प्रूफ की लंबाई $\tau$ .

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

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

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

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

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

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

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

पत्राचार स्टीफन कुक (1975) द्वारा प्रस्तुत किया गया था, जिन्होंने औपचारिक रूप से उस सीओएनपी प्रमेय को दिखाया था $\Pi _{1}^{b}$ सूत्र, सिद्धांत के $\mathrm {PV} _{1}$ विस्तारित फ़्रीज में बहुपद-आकार के प्रमाणों के साथ टॉटोलॉजी के अनुक्रमों का अनुवाद करें। इसके अलावा, ्सटेंडेड फ्रीज ऐसी सबसे कमजोर प्रणाली है: यदि किसी अन्य प्रूफ सिस्टम पी में यह संपत्ति है, तो पी ्सटेंडेड फ्रीज का अनुकरण करता है।^[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) ने साबित किया कि ्सटेंडेड फ्रीज तब तक व्यवहार्य इंटरपोलेशन को स्वीकार नहीं करता जब तक कि आरएसए पी/पॉली के खिलाफ सुरक्षित न हो।^[31]
बोनेट, पिटासी और रज़ (2000) ने साबित किया कि $TC^{0}$ -फ्रेज सिस्टम तब तक व्यवहार्य प्रक्षेप को स्वीकार नहीं करता जब तक कि डिफी-हेलमैन योजना पी/पॉली के खिलाफ सुरक्षित न हो।^[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 1: / Line 1: @@
-[[तर्क]] और [[सैद्धांतिक कंप्यूटर विज्ञान]] में, और विशेष रूप से [[प्रमाण सिद्धांत]] और [[कम्प्यूटेशनल जटिलता सिद्धांत]] में, प्रमाण जटिलता वह क्षेत्र है जिसका लक्ष्य उन कम्प्यूटेशनल संसाधनों को समझना और उनका विश्लेषण करना है जो बयानों को साबित करने या खंडन करने के लिए आवश्यक हैं। प्रमाण जटिलता में अनुसंधान मुख्य रूप से विभिन्न प्रस्ताव प्रमाण प्रणालियों में प्रमाण-लंबाई की निचली और ऊपरी सीमा को साबित करने से संबंधित है। उदाहरण के लिए, प्रमाण जटिलता की प्रमुख चुनौतियों में से एक यह दर्शाना है कि फ़्रीज प्रणाली, सामान्य [[प्रस्तावात्मक कलन]], सभी तनातनी के बहुपद-आकार के प्रमाणों को स्वीकार नहीं करती है। यहां प्रमाण का आकार केवल उसमें प्रतीकों की संख्या है, और एक प्रमाण को बहुपद आकार का कहा जाता है यदि यह टॉटोलॉजी के आकार में बहुपद है जो इसे साबित करता है।
+[[तर्क]] और [[सैद्धांतिक कंप्यूटर विज्ञान]] में, और विशेष रूप से [[प्रमाण सिद्धांत]] और [[कम्प्यूटेशनल जटिलता सिद्धांत]] में, प्रमाण जटिलता वह क्षेत्र है जिसका लक्ष्य उन कम्प्यूटेशनल संसाधनों को समझना और उनका विश्लेषण करना है जो बयानों को साबित करने या खंडन करने के लिए आवश्यक हैं। प्रमाण जटिलता में अनुसंधान मुख्य रूप से विभिन्न प्रस्ताव प्रमाण प्रणालियों में प्रमाण-लंबाई की निचली और ऊपरी सीमा को साबित करने से संबंधित है। उदाहरण के लिए, प्रमाण जटिलता की प्रमुख चुनौतियों में से  यह दर्शाना है कि फ़्रीज प्रणाली, सामान्य [[प्रस्तावात्मक कलन]], सभी तनातनी के बहुपद-आकार के प्रमाणों को स्वीकार नहीं करती है। यहां प्रमाण का आकार केवल उसमें प्रतीकों की संख्या है, और  प्रमाण को बहुपद आकार का कहा जाता है यदि यह टॉटोलॉजी के आकार में बहुपद है जो इसे साबित करता है।
-प्रमाण जटिलता का व्यवस्थित अध्ययन [[स्टीफन कुक]] और [[रॉबर्ट रेकहो]] (1979) के काम से शुरू हुआ, जिन्होंने कम्प्यूटेशनल जटिलता के परिप्रेक्ष्य से एक [[प्रस्ताव प्रमाण प्रणाली]] की मूल परिभाषा प्रदान की। विशेष रूप से कुक और रेकहो ने देखा कि मजबूत और मजबूत प्रपोजल [[फ्रीज प्रणाली]] पर प्रूफ साइज की निचली सीमा साबित करने को [[एन[[पी (जटिलता)]]]] को सीओएनपी से अलग करने की दिशा में एक कदम के रूप में देखा जा सकता है (और इस प्रकार एनपी से पी (जटिलता)), क्योंकि एक प्रपोजल प्रूफ सिस्टम का अस्तित्व जो सभी टॉटोलॉजी के लिए बहुपद आकार के सबूतों को स्वीकार करता है, एनपी = सीओएनपी के बराबर है।
+प्रमाण जटिलता का व्यवस्थित अध्ययन [[स्टीफन कुक]] और [[रॉबर्ट रेकहो]] (1979) के काम से शुरू हुआ, जिन्होंने कम्प्यूटेशनल जटिलता के परिप्रेक्ष्य से  [[प्रस्ताव प्रमाण प्रणाली]] की मूल परिभाषा प्रदान की। विशेष रूप से कुक और रेकहो ने देखा कि मजबूत और मजबूत प्रपोजल [[फ्रीज प्रणाली]] पर प्रूफ साइज की निचली सीमा साबित करने को [[एन[[पी (जटिलता)]]]] को सीओएनपी से अलग करने की दिशा में  कदम के रूप में देखा जा सकता है (और इस प्रकार एनपी से पी (जटिलता)), क्योंकि  प्रपोजल प्रूफ सिस्टम का अस्तित्व जो सभी टॉटोलॉजी के लिए बहुपद आकार के सबूतों को स्वीकार करता है, एनपी = सीओएनपी के बराबर है।
 समसामयिक प्रमाण जटिलता अनुसंधान कम्प्यूटेशनल जटिलता, [[कलन विधि]] और गणित के कई क्षेत्रों से विचार और विधियाँ प्राप्त करता है। चूंकि कई महत्वपूर्ण एल्गोरिदम और एल्गोरिदमिक तकनीकों को कुछ प्रूफ सिस्टम के लिए प्रूफ खोज एल्गोरिदम के रूप में डाला जा सकता है, इसलिए इन सिस्टम में प्रूफ आकार पर निचली सीमा साबित करने से संबंधित एल्गोरिदम पर रन-टाइम निचली सीमा का पता चलता है। यह प्रूफ जटिलता को SAT सॉल्वर जैसे अधिक लागू क्षेत्रों से जोड़ता है।
-[[गणितीय तर्क]] प्रस्तावित प्रमाण आकारों का अध्ययन करने के लिए एक रूपरेखा के रूप में भी काम कर सकता है। [[प्रथम-क्रम सिद्धांत]] और, विशेष रूप से, [[पीनो अंकगणित]] के कमजोर टुकड़े, जो बंधे हुए अंकगणित के नाम से आते हैं, प्रस्ताव प्रमाण प्रणालियों के समान संस्करणों के रूप में कार्य करते हैं और व्यवहार्य तर्क के विभिन्न स्तरों के संदर्भ में लघु प्रस्ताव प्रमाणों की व्याख्या के लिए आगे की पृष्ठभूमि प्रदान करते हैं।
+[[गणितीय तर्क]] प्रस्तावित प्रमाण आकारों का अध्ययन करने के लिए  रूपरेखा के रूप में भी काम कर सकता है। [[प्रथम-क्रम सिद्धांत]] और, विशेष रूप से, [[पीनो अंकगणित]] के कमजोर टुकड़े, जो बंधे हुए अंकगणित के नाम से आते हैं, प्रस्ताव प्रमाण प्रणालियों के समान संस्करणों के रूप में कार्य करते हैं और व्यवहार्य तर्क के विभिन्न स्तरों के संदर्भ में लघु प्रस्ताव प्रमाणों की व्याख्या के लिए आगे की पृष्ठभूमि प्रदान करते हैं।
 ==प्रमाण प्रणालियाँ==
 {{Main|propositional proof system}}
-एक प्रस्तावक प्रमाण प्रणाली को दो इनपुट के साथ प्रमाण-सत्यापन एल्गोरिथ्म P(A,x) के रूप में दिया गया है। यदि P जोड़ी (A,x) को स्वीकार करता है तो हम कहते हैं कि x, A का P-प्रमाण है।
+प्रस्तावक प्रमाण प्रणाली को दो इनपुट के साथ प्रमाण-सत्यापन एल्गोरिथ्म P(A,x) के रूप में दिया गया है। यदि P जोड़ी (A,x) को स्वीकार करता है तो हम कहते हैं कि x, A का P-प्रमाण है।
-प्रोपोज़िशनल प्रूफ सिस्टम के उदाहरणों में अनुक्रमिक कैलकुलस, रिज़ॉल्यूशन (तर्क), [[कटिंग-प्लेन विधि]] और फ़्रीज सिस्टम शामिल हैं। [[ज़र्मेलो फ्रेंकेल सेट सिद्धांत]] जैसे मजबूत गणितीय सिद्धांत प्रस्तावात्मक प्रमाण प्रणालियों को भी प्रेरित करते हैं: एक टॉटोलॉजी का प्रमाण <math>\tau</math> ZFC की प्रस्तावात्मक व्याख्या में एक औपचारिक कथन का ZFC-प्रमाण है '<math>\tau</math> एक तनातनी है'.
+प्रोपोज़िशनल प्रूफ सिस्टम के उदाहरणों में अनुक्रमिक कैलकुलस, रिज़ॉल्यूशन (तर्क), [[कटिंग-प्लेन विधि]] और फ़्रीज सिस्टम शामिल हैं। [[ज़र्मेलो फ्रेंकेल सेट सिद्धांत]] जैसे मजबूत गणितीय सिद्धांत प्रस्तावात्मक प्रमाण प्रणालियों को भी प्रेरित करते हैं:  टॉटोलॉजी का प्रमाण <math>\tau</math> ZFC की प्रस्तावात्मक व्याख्या में  औपचारिक कथन का ZFC-प्रमाण है '<math>\tau</math>  तनातनी है'.
 ==बहुपद आकार के प्रमाण और एनपी बनाम सीओएनपी समस्या==
-प्रूफ़ जटिलता आमतौर पर किसी दिए गए टॉटोलॉजी के लिए सिस्टम में संभव प्रूफ़ों के न्यूनतम आकार के संदर्भ में प्रूफ़ प्रणाली की दक्षता को मापती है। एक प्रमाण का आकार (क्रमशः सूत्र) प्रमाण (क्रमशः सूत्र) का प्रतिनिधित्व करने के लिए आवश्यक प्रतीकों की संख्या है। यदि कोई स्थिरांक मौजूद है तो एक प्रस्ताव प्रमाण प्रणाली P बहुपद रूप से परिबद्ध है <math>c</math> ऐसा कि आकार की हर तनातनी <math>n</math> आकार का पी-प्रूफ़ है <math>(n+c)^c</math>. प्रमाण जटिलता का एक केंद्रीय प्रश्न यह समझना है कि क्या टॉटोलॉजी बहुपद-आकार के प्रमाणों को स्वीकार करती है। औपचारिक रूप से,
+प्रूफ़ जटिलता आमतौर पर किसी दिए गए टॉटोलॉजी के लिए सिस्टम में संभव प्रूफ़ों के न्यूनतम आकार के संदर्भ में प्रूफ़ प्रणाली की दक्षता को मापती है।  प्रमाण का आकार (क्रमशः सूत्र) प्रमाण (क्रमशः सूत्र) का प्रतिनिधित्व करने के लिए आवश्यक प्रतीकों की संख्या है। यदि कोई स्थिरांक मौजूद है तो  प्रस्ताव प्रमाण प्रणाली P बहुपद रूप से परिबद्ध है <math>c</math> ऐसा कि आकार की हर तनातनी <math>n</math> आकार का पी-प्रूफ़ है <math>(n+c)^c</math>. प्रमाण जटिलता का  केंद्रीय प्रश्न यह समझना है कि क्या टॉटोलॉजी बहुपद-आकार के प्रमाणों को स्वीकार करती है। औपचारिक रूप से,
 <ब्लॉककोट>समस्या (एनपी बनाम सीओएनपी)
@@ Line 21: / Line 21: @@
 </ब्लॉककोट>
-कुक और रेकहो (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>
+कुक और रेकहो (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>
+== प्रमाण प्रणालियों के बीच इष्टतमता और सिमुलेशन ==
-==प्रमाण प्रणालियों के बीच इष्टतमता और सिमुलेशन==
+प्रूफ जटिलता सिमुलेशन की धारणा का उपयोग करके प्रूफ सिस्टम की ताकत की तुलना करती है।  प्रूफ सिस्टम पी पी  प्रूफ सिस्टम क्यू का अनुकरण करता है यदि कोई बहुपद-समय फ़ंक्शन है जो  टॉटोलॉजी का क्यू-प्रूफ देता है तो उसी टॉटोलॉजी का  पी-प्रूफ आउटपुट करता है। यदि पी पी-क्यू का अनुकरण करता है और क्यू पी-पी का अनुकरण करता है, तो प्रमाण प्रणाली पी और क्यू पी-समतुल्य हैं। सिमुलेशन की  कमजोर धारणा भी है:  प्रूफ सिस्टम पी  प्रूफ सिस्टम क्यू का अनुकरण करता है यदि कोई बहुपद पी है जैसे कि टॉटोलॉजी ए के प्रत्येक क्यू-प्रूफ ्स के लिए, ए का  पी-प्रूफ वाई है जैसे कि वाई की लंबाई, |y| अधिकतम p(|x|) है।
-प्रूफ जटिलता सिमुलेशन की धारणा का उपयोग करके प्रूफ सिस्टम की ताकत की तुलना करती है। एक प्रूफ सिस्टम पी पी एक प्रूफ सिस्टम क्यू का अनुकरण करता है यदि कोई बहुपद-समय फ़ंक्शन है जो एक टॉटोलॉजी का क्यू-प्रूफ देता है तो उसी टॉटोलॉजी का एक पी-प्रूफ आउटपुट करता है। यदि पी पी-क्यू का अनुकरण करता है और क्यू पी-पी का अनुकरण करता है, तो प्रमाण प्रणाली पी और क्यू पी-समतुल्य हैं। सिमुलेशन की एक कमजोर धारणा भी है: एक प्रूफ सिस्टम पी एक प्रूफ सिस्टम क्यू का अनुकरण करता है यदि कोई बहुपद पी है जैसे कि टॉटोलॉजी ए के प्रत्येक क्यू-प्रूफ एक्स के लिए, ए का एक पी-प्रूफ वाई है जैसे कि वाई की लंबाई, |y| अधिकतम p(|x|) है।
 उदाहरण के लिए, अनुक्रमिक कैलकुलस (प्रत्येक) फ़्रीज प्रणाली के लिए पी-समतुल्य है।<ref name="Rec">{{cite thesis|first1=Robert A.|last1=Reckhow|title=प्रस्तावात्मक गणना में प्रमाणों की लंबाई पर|type=PhD Thesis |publisher=University of Toronto |year=1976}}</ref>
-एक प्रूफ सिस्टम पी-इष्टतम है यदि यह अन्य सभी प्रूफ सिस्टमों का पी-अनुकरण करता है, और यह इष्टतम है यदि यह अन्य सभी प्रूफ सिस्टमों का अनुकरण करता है। यह एक खुली समस्या है कि क्या ऐसी प्रमाण प्रणालियाँ मौजूद हैं:
+प्रूफ सिस्टम पी-इष्टतम है यदि यह अन्य सभी प्रूफ सिस्टमों का पी-अनुकरण करता है, और यह इष्टतम है यदि यह अन्य सभी प्रूफ सिस्टमों का अनुकरण करता है। यह  खुली समस्या है कि क्या ऐसी प्रमाण प्रणालियाँ मौजूद हैं:
 <ब्लॉककोट>'समस्या' (इष्टतमता)
@@ Line 35: / Line 33: @@
 </ब्लॉककोट>
-प्रत्येक प्रस्ताव प्रमाण प्रणाली पी को फ़्रीज प्रणाली # विस्तारित फ़्रीज प्रणाली द्वारा अनुकरण किया जा सकता है जो पी की सुदृढ़ता को अभिगृहीत करने वाले सिद्धांतों के साथ विस्तारित है।<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="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>
+== प्रमाण खोज की स्वचालितता ==
-==प्रमाण खोज की स्वचालितता==
+प्रमाण जटिलता में  महत्वपूर्ण प्रश्न प्रमाण प्रणालियों में प्रमाण खोजने की जटिलता को समझना है।
-प्रमाण जटिलता में एक महत्वपूर्ण प्रश्न प्रमाण प्रणालियों में प्रमाण खोजने की जटिलता को समझना है।
 <ब्लॉककोट>समस्या (स्वचालितता)
@@ Line 48: / Line 44: @@
 प्रश्न को स्वचालितता (जिसे स्वचालितता के रूप में भी जाना जाता है) की धारणा द्वारा औपचारिक रूप दिया जा सकता है।<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>.
+प्रूफ सिस्टम पी स्वचालित है यदि कोई एल्गोरिदम है जो  टॉटोलॉजी देता है <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>
+* क्रेजीसेक और पुडलक (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>
-* मारिया लुइसा बोनेट, [[टोनियान पिटासी]] और [[एक बार घाव]] (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>-फ्रेज सिस्टम कमजोर रूप से स्वचालित नहीं है जब तक कि कुंजी ्सचेंज|डिफी-हेलमैन योजना पी/पॉली के खिलाफ सुरक्षित न हो।<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>
 * एटसेरियस और मुलर (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>
@@ Line 62: / Line 58: @@
 * बीम और पिटासी (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|Bounded arithmetic}}
 प्रस्तावित प्रमाण प्रणालियों की व्याख्या उच्च क्रम के सिद्धांतों के गैर-समान समकक्षों के रूप में की जा सकती है। समतुल्यता का अध्ययन अक्सर परिबद्ध अंकगणित के सिद्धांतों के संदर्भ में किया जाता है। उदाहरण के लिए, विस्तारित फ्रीज प्रणाली कुक के सिद्धांत से मेल खाती है <math>\mathrm {PV}_1</math> बहुपद-समय तर्क को औपचारिक बनाना और फ़्रीज प्रणाली सिद्धांत से मेल खाती है <math>\mathrm {VNC}^1</math> एनसी (जटिलता) को औपचारिक बनाना#एनसी पदानुक्रम|<math>\mathsf{NC}^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>\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 73: @@
   | 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}}
-टॉटोलॉजी को पहचानने के लिए प्रपोजल प्रूफ सिस्टम की व्याख्या गैर-नियतात्मक एल्गोरिदम के रूप में की जा सकती है। एक प्रमाण प्रणाली पी पर एक सुपरपोलिनोमियल निचली सीमा साबित करना इस प्रकार पी के आधार पर एसएटी के लिए एक बहुपद-समय एल्गोरिदम के अस्तित्व को खारिज कर देता है। उदाहरण के लिए, असंतोषजनक उदाहरणों पर [[डीपीएलएल एल्गोरिदम]] का रन पेड़-जैसे संकल्प खंडन के अनुरूप होता है। इसलिए, पेड़-जैसे रिज़ॉल्यूशन (नीचे देखें) के लिए घातीय निचली सीमाएं SAT के लिए कुशल डीपीएलएल एल्गोरिदम के अस्तित्व को खारिज करती हैं। इसी प्रकार, घातीय रिज़ॉल्यूशन निचली सीमा का अर्थ है कि रिज़ॉल्यूशन पर आधारित SAT सॉल्वर, जैसे कि संघर्ष-संचालित क्लॉज लर्निंग एल्गोरिदम, SAT को कुशलतापूर्वक (सबसे खराब स्थिति में) हल नहीं कर सकते हैं।
+टॉटोलॉजी को पहचानने के लिए प्रपोजल प्रूफ सिस्टम की व्याख्या गैर-नियतात्मक एल्गोरिदम के रूप में की जा सकती है।  प्रमाण प्रणाली पी पर  सुपरपोलिनोमियल निचली सीमा साबित करना इस प्रकार पी के आधार पर एसएटी के लिए  बहुपद-समय एल्गोरिदम के अस्तित्व को खारिज कर देता है। उदाहरण के लिए, असंतोषजनक उदाहरणों पर [[डीपीएलएल एल्गोरिदम]] का रन पेड़-जैसे संकल्प खंडन के अनुरूप होता है। इसलिए, पेड़-जैसे रिज़ॉल्यूशन (नीचे देखें) के लिए घातीय निचली सीमाएं SAT के लिए कुशल डीपीएलएल एल्गोरिदम के अस्तित्व को खारिज करती हैं। इसी प्रकार, घातीय रिज़ॉल्यूशन निचली सीमा का अर्थ है कि रिज़ॉल्यूशन पर आधारित SAT सॉल्वर, जैसे कि संघर्ष-संचालित क्लॉज लर्निंग एल्गोरिदम, SAT को कुशलतापूर्वक (सबसे खराब स्थिति में) हल नहीं कर सकते हैं।
 ==निचली सीमा==
@@ Line 90: / Line 84: @@
 प्रस्तावित प्रमाणों की लंबाई पर निचली सीमा साबित करना आम तौर पर बहुत मुश्किल होता है। फिर भी, कमजोर प्रूफ सिस्टम के लिए निचली सीमा साबित करने के कई तरीके खोजे गए हैं।
-* हेकेन (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>
+* हेकेन (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="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>[[सर्किट जटिलता]] में निचली सीमाएं।
+* अजताई (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>
+* लेस (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>
+* बेन-सैसन और विगडरसन (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>. टॉटोलॉजी प्रत्येक विकल्प के लिए सत्य है <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> कुछ प्रमाण प्रणाली में एक संक्षिप्त प्रमाण है; (बी) ऐसी प्रमाण प्रणाली में व्यवहार्य प्रक्षेप है; (सी) इंटरपोलेंट सर्किट एक कम्प्यूटेशनल रूप से कठिन समस्या का समाधान करता है। यह स्पष्ट है कि (ए) और (बी) का अर्थ है कि एक छोटा इंटरपोलेंट सर्किट है, जो (सी) के साथ विरोधाभास में है। इस तरह का संबंध गणनाओं पर प्रूफ लंबाई की ऊपरी सीमा को निचली सीमा में बदलने की अनुमति देता है, और कुशल इंटरपोलेशन एल्गोरिदम को प्रूफ लंबाई पर निचली सीमा में बदलने की अनुमति देता है।
+निम्नलिखित तीन कथन  साथ सत्य नहीं हो सकते: (ए) <math>A(x,y) \rightarrow B(y,z)</math> कुछ प्रमाण प्रणाली में  संक्षिप्त प्रमाण है; (बी) ऐसी प्रमाण प्रणाली में व्यवहार्य प्रक्षेप है; (सी) इंटरपोलेंट सर्किट  कम्प्यूटेशनल रूप से कठिन समस्या का समाधान करता है। यह स्पष्ट है कि (ए) और (बी) का अर्थ है कि  छोटा इंटरपोलेंट सर्किट है, जो (सी) के साथ विरोधाभास में है। इस तरह का संबंध गणनाओं पर प्रूफ लंबाई की ऊपरी सीमा को निचली सीमा में बदलने की अनुमति देता है, और कुशल इंटरपोलेशन एल्गोरिदम को प्रूफ लंबाई पर निचली सीमा में बदलने की अनुमति देता है।
 कुछ प्रूफ सिस्टम जैसे रेजोल्यूशन और कटिंग प्लेन व्यवहार्य प्रक्षेप या इसके वेरिएंट को स्वीकार करते हैं।<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) ने साबित किया कि ्सटेंडेड फ्रीज तब तक व्यवहार्य इंटरपोलेशन को स्वीकार नहीं करता जब तक कि आरएसए पी/पॉली के खिलाफ सुरक्षित न हो।<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>
 * बोनेट, डोमिंगो, गवाल्डा, मैकिएल, पिटासी (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>
-==यह भी देखें==
+== यह भी देखें ==
 *कम्प्यूटेशनल जटिलता सिद्धांत
 *सर्किट जटिलता

Anonymous

Search

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

Namespaces

More

Page actions

Revision as of 23:50, 4 August 2023

Contents

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

बहुपद आकार के प्रमाण और एनपी बनाम सीओएनपी समस्या

प्रमाण प्रणालियों के बीच इष्टतमता और सिमुलेशन

प्रमाण खोज की स्वचालितता

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

सैट सॉल्वर

निचली सीमा

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

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

यह भी देखें

संदर्भ

अग्रिम पठन

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

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

Revision as of 23:50, 4 August 2023

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

बहुपद आकार के प्रमाण और एनपी बनाम सीओएनपी समस्या

प्रमाण प्रणालियों के बीच इष्टतमता और सिमुलेशन

प्रमाण खोज की स्वचालितता

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

सैट सॉल्वर

निचली सीमा

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

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

यह भी देखें

संदर्भ

अग्रिम पठन

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories