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

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

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

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

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

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

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

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

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

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

प्रॉब्लम (NP के प्रति coNP)

क्या बहुपद से परिबद्ध प्रोपोज़िशनल प्रूफ सिस्टम उपस्थित है?

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

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

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

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

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

प्रॉब्लम (ऑप्टिमालिटी)

क्या कोई p-ऑप्टिमालिटी या ऑप्टिमालिटी प्रस्तावक प्रूफ सिस्टम उपस्थित है?

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

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

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

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

प्रॉब्लम (ऑटोमैटाबिलिटी)

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

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

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

माना जाता है कि ब्याज की कई प्रूफ सिस्टम्स गैर-ऑटोमेटिक हैं। यद्यपि, वर्तमान में केवल प्रतिबंधात्मक ऋणात्मक परिणाम ही ज्ञात हैं।

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

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

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

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

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

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

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

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

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

सैट सॉल्वर

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

लोअर बाउंड

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

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

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

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

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

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

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

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

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

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

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

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

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

यह भी देखें

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

संदर्भ

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

अग्रिम पठन

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

बाहरी संबंध

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

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

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

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

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

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

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

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

[BDGMP-9] Bonet, M.L.; Domingo, C.; Gavaldá, R.; Maciel, A.; Pitassi, Toniann (2004). "बाउंडेड-डेप्थ फ़्रीज प्रूफ़ की गैर-स्वचालितता". Computational Complexity. 13 (1–2): 47–68. doi:10.1007/s00037-004-0183-5. S2CID 1360759.

[AleRaz-10] Alekhnovich, Michael; Razborov, Alexander (2018). "Resolution is not automatizable unless W[P] is tractable". SIAM Journal on Computing. 38 (4): 1347–1363. doi:10.1137/06066850X.

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

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

[AM-13] Atserias, Albert; Müller, Moritz (2019). "Automating resolution is NP-hard". Proceedings of the 60th Symposium on Foundations of Computer Science. pp. 498–509.

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

[GKMP-15] Göös, Mika; Koroth, Sajin; Mertz, Ian; Pitassi, Tonnian (2020). "कटिंग विमानों को स्वचालित करना एनपी-हार्ड है". STOC: 68–77. arXiv:2004.08037. doi:10.1145/3357713.3384248. ISBN 9781450369794. S2CID 215814356.

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

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

[BW-18] 18.0 ^18.1 Ben-Sasson, Eli; Wigderson, Avi (1999). "Short proofs are narrow - resolution made simple". Proceedings of the 31st ACM Symposium on Theory of Computing. pp. 517–526.

[cook-19] Cook, Stephen (1975). "Feasibly constructive proofs and the propositiona calculus". Proceedings of the 7th Annual ACM Symposium on Theory of Computing. pp. 83–97.

[PW-20] Paris, Jeff; Wilkie, Alex (1985). "परिबद्ध अंकगणित में समस्याएँ गिनना". Methods in Mathematical Logic. Lecture Notes in Mathematics. 1130: 317–340. doi:10.1007/BFb0075316. ISBN 978-3-540-15236-1.

[CN-21] Cook, Stephen; Nguyen, Phuong (2010). Logical Foundations of Proof Complexity. Perspectives in Logic. Cambridge: Cambridge University Press. doi:10.1017/CBO9780511676277. ISBN 978-0-521-51729-4. MR 2589550. (draft from 2008)

[Ajt-22] Ajtai, M. (1988). "The complexity of the pigeonhole principle". Proceedings of the IEEE 29th Annual Symposium on Foundation of Computer Science. pp. 346–355.

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

[Ajtb-24] Ajtai, M. (1988). "The complexity of the pigeonhole principle". Proceedings of the IEEE 29th Annual Symposium on Foundation of Computer Science. pp. 346–355.

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

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

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

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

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

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

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

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

[BDGMPb-33] Bonet, M.L.; Domingo, C.; Gavaldá, R.; Maciel, A.; Pitassi, Toniann (2004). "बाउंडेड-डेप्थ फ़्रीज प्रूफ़ की गैर-स्वचालितता". Computational Complexity. 13 (1–2): 47–68. doi:10.1007/s00037-004-0183-5. S2CID 1360759.

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

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

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

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29]

[30]

[31]

[32]

[33]

[34]

[35]

[36]