प्रूफ कॉम्पलेक्सिटी

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

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

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

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

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

Main article: प्रस्ताव प्रमाण प्रणाली

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

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

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

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

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

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

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

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

प्रूफ कॉम्पलेक्सिटी सिमुलेशन की धारणा का उपयोग करके प्रूफ सिस्टम के सामर्थ्य की उपमा करती है। प्रूफ सिस्टम 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-समतुल्य है।

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

पत्राचार स्टीफन कुक (1975) द्वारा प्रस्तुत किया गया था, जिन्होंने औपचारिक रूप से उस सीओएनपी प्रमेय को दिखाया था $\Pi _{1}^{b}$ सूत्र, सिद्धांत के $\mathrm {PV} _{1}$ विस्तारित फ़्रीज में बहुपद-आकार के प्रमाणों के साथ टॉटोलॉजी के अनुक्रमों का अनुवाद करें। इसके अलावा, ्सटेंडेड फ्रीज ऐसी सबसे कमजोर प्रणाली है: यदि किसी अन्य प्रूफ सिस्टम पी में यह संपत्ति है, तो पी ्सटेंडेड फ्रीज का अनुकरण करता है। जेफ पेरिस (गणितज्ञ) और एलेक्स विल्की (1985) द्वारा दिए गए दूसरे क्रम के तर्क | दूसरे क्रम के बयानों और प्रस्ताव सूत्रों के मध्य वैकल्पिक अनुवाद विस्तारित फ्रीज जैसे फ्रीज या निरंतर-गहराई फ्रीज के उप-प्रणालियों को कैप्चर करने के लिए अधिक व्यावहारिक रहा है। जबकि उपर्युक्त पत्राचार कहता है कि सिद्धांत में प्रमाण संबंधित प्रमाण प्रणाली में लघु प्रमाणों के अनुक्रम में तब्दील हो जाते हैं, विपरीत निहितार्थ का रूप भी लागू होता है। सिस्टम पी के अनुरूप सिद्धांत टी के उपयुक्त मॉडल (तर्क) का निर्माण करके प्रमाण प्रणाली पी में प्रमाण के आकार पर निचली सीमा प्राप्त करना संभव है। यह मॉडल-सैद्धांतिक निर्माणों के माध्यम से कॉम्पलेक्सिटी की निचली सीमा को सिद्ध करने की अनुमति देता है, दृष्टिकोण जिसे मिक्लोस अजताई की विधि के रूप में जाना जाता है।

सैट सॉल्वर

See also: SAT solver

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

निचली सीमा

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

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

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

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

प्रपत्र की तनातनी पर विचार करें $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)$ कुछ प्रमाण प्रणाली में संक्षिप्त प्रमाण है; (बी) ऐसी प्रमाण प्रणाली में व्यवहार्य प्रक्षेप है; (सी) इंटरपोलेंट सर्किट कम्प्यूटेशनल रूप से कठिन समस्या का समाधान करता है। यह स्पष्ट है कि (ए) और (बी) का अर्थ है कि छोटा इंटरपोलेंट सर्किट है, जो (सी) के साथ विरोधाभास में है। इस तरह का संबंध गणनाओं पर प्रूफ लंबाई की ऊपरी सीमा को निचली सीमा में बदलने की अनुमति देता है, और कुशल इंटरपोलेशन एल्गोरिदम को प्रूफ लंबाई पर निचली सीमा में बदलने की अनुमति देता है।

कुछ प्रूफ सिस्टम जैसे रेजोल्यूशन और कटिंग प्लेन व्यवहार्य प्रक्षेप या इसके वेरिएंट को स्वीकार करते हैं। व्यवहार्य प्रक्षेप को स्वचालितता के कमजोर रूप के रूप में देखा जा सकता है। वास्तव में, कई प्रमाण प्रणालियों के लिए, जैसे कि विस्तारित फ़्रीज, व्यवहार्य प्रक्षेप कमजोर स्वचालितता के बराबर है। विशेष रूप से, कई प्रमाण प्रणालियाँ 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$. इस तरह के इंटरपोलेंट का उपयोग प्रूफ सिस्टम आर को परिभाषित करने के लिए किया जा सकता है जो दर्शाता है कि पी कमजोर रूप से स्वचालित है। दूसरी ओर, प्रमाण प्रणाली पी की कमजोर स्वचालितता का तात्पर्य है कि पी व्यवहार्य प्रक्षेप को स्वीकार करता है। यद्यपि, यदि कोई प्रूफ सिस्टम पी अपनी स्वयं की सुदृढ़ता को कुशलता से सिद्ध नहीं करता है, तो यह व्यवहार्य प्रक्षेप को स्वीकार करने पर भी कमजोर रूप से स्वचालित नहीं हो सकता है।

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

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

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

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

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

यह भी देखें

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

अग्रिम पठन

• 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

बाहरी संबंध

• Proof Complexity
• Proof complexity mailing list.