Resolution proof reduction via local context rewriting
प्रमाण सिद्धांत में, गणितीय तर्क का एक क्षेत्र, स्थानीय संदर्भ पुनर्लेखन के माध्यम से संकल्प प्रमाण में कमी, स्थानीय संदर्भ पुनर्लेखन के माध्यम से संकल्प प्रमाण में कमी के लिए एक तकनीक है। इस प्रूफ कम्प्रेशन विधि को रिड्यूस एंड रिकंस्ट्रक्ट नामक एक एल्गोरिथ्म के रूप में प्रस्तुत किया गया था, जो रिज़ॉल्यूशन प्रूफ के पोस्ट-प्रोसेसिंग के रूप में काम करता है। रिड्यूस एंड रिकंस्ट्रक्ट स्थानीय प्रूफ पुनर्लेखन नियमों के एक समूह पर आधारित है जो एक सबप्रूफ को समकक्ष या मजबूत में बदल देता है। प्रत्येक नियम को एक विशिष्ट संदर्भ से मेल खाने के लिए परिभाषित किया गया है। एक संदर्भ में दो धुरी (और) और पाँच खंड (,, और) शामिल हैं। एक संदर्भ की संरचना () में दिखाई गई है। ध्यान दें कि इसका तात्पर्य यह है कि यह और (विपरीत ध्रुवीयता के साथ) में निहित है और और (विपरीत ध्रुवीयता के साथ भी) में निहित है। नीचे दी गई तालिका सिमोन एट अल द्वारा प्रस्तावित पुनर्लेखन नियमों को दर्शाती है। एल्गोरिथम का विचार इन नियमों को अवसरवादी रूप से लागू करके प्रमाण आकार को कम करना है। पहले पाँच नियमों को पहले के पेपर में पेश किया गया था। इसके अलावाः नियम ए2 अपने आप में कोई कमी नहीं करता है। हालाँकि, यह अभी भी उपयोगी है, क्योंकि इसका "फेरबदल" प्रभाव अन्य नियमों को लागू करने के लिए नए अवसर पैदा कर सकता है; नियम ए1 का उपयोग व्यवहार में नहीं किया जाता है, क्योंकि यह प्रमाण आकार को बढ़ा सकता है; नियम बी1, बी2, बी2 'और बी3 कमी के लिए सीधे तौर पर जिम्मेदार हैं, क्योंकि वे मूल की तुलना में मजबूत रूप से एक परिवर्तित मूल खंड का उत्पादन करते हैं; बी नियम के अनुप्रयोग से एक अवैध प्रमाण हो सकता है (नीचे उदाहरण देखें), क्योंकि परिवर्तित मूल खंड में गायब कुछ अक्षर प्रमाण मूल के रास्ते में एक और संकल्प चरण में शामिल हो सकते हैं। इसलिए, जब ऐसा होता है तो एल्गोरिथ्म को एक कानूनी प्रमाण का "पुनर्निर्माण" भी करना पड़ता है। निम्नलिखित उदाहरण एक ऐसी स्थिति को दर्शाता है जहां बी2 'नियम के लागू होने के बाद प्रमाण अवैध हो जाता हैः हाइलाइट किए गए संदर्भ में नियम बी2' को लागू करनाः प्रमाण अब अवैध है क्योंकि परिवर्तित मूल खंड से शाब्दिक गायब है। प्रमाण के पुनर्निर्माण के लिए, कोई भी अंतिम समाधान चरण (जो अब अनावश्यक है) के साथ एक साथ हटा सकता है। अंतिम परिणाम निम्नलिखित कानूनी (और मजबूत) प्रमाण हैः नियम बी 2 'को लागू करने का एक नया अवसर बनाने के लिए नियम ए 2 को लागू करके इस प्रमाण में और कमी। आमतौर पर बड़ी संख्या में ऐसे संदर्भ होते हैं जहां नियम ए2 लागू किया जा सकता है, इसलिए एक संपूर्ण दृष्टिकोण सामान्य रूप से संभव नहीं है। एक प्रस्ताव दो समाप्ति मानदंडों के साथ एक लूप के रूप में रिड्यूस एंड रिकंस्ट्रक्ट को निष्पादित करना हैः पुनरावृत्तियों की संख्या और एक टाइमआउट (जो पहले प्राप्त किया जाता है)। नीचे दिया गया छद्म कोड इसे दर्शाता है। 1 फलन रिड्यूस एंड रिकंस्ट्रक्ट (/* एक प्रमाण */, समय सीमा, अधिकतम पुनरावृत्तियाँ): i = 1 के लिए 2 अधिकतम पुनरावृत्तियों के लिए 3 रिड्यूस एंड रिकंस्ट्रक्ट लूप () करें; 4 यदि समय> समय सीमा तो// टाइमआउट 5 ब्रेक; 7 अंतिम फलन रिड्यूस एंड रिकंस्ट्रक्ट के लिए 6 अंत रिड्यूस एंड रिकंस्ट्रक्ट लूप फ़ंक्शन का उपयोग करता है, जो नीचे निर्दिष्ट है। एल्गोरिदम का पहला भाग रिज़ॉल्यूशन ग्राफ का एक टोपोलॉजिकल ऑर्डर करता है (यह देखते हुए कि किनारे पूर्ववर्ती से रिज़ॉल्वेंट तक जाते हैं)। यह सुनिश्चित करने के लिए किया जाता है कि प्रत्येक नोड को उसके पूर्ववर्तियों के बाद देखा जाता है (इस तरह, टूटे हुए रिज़ॉल्यूशन चरणों को हमेशा पाया और तय किया जाता है)। 1 फलन रिड्यूस एंड रिकंस्ट्रक्ट लूप (/* एक प्रमाण */): 2 टी. एस. = टोपोलॉजिकल सॉर्टिंग (); टी. एस. 4 में प्रत्येक नोड के लिए 3 यदि एक पत्ती नहीं है 5 यदि और फिर 6 = रिज़ॉल्यूशन (,); 7 के बाएं संदर्भ का निर्धारण करें, यदि कोई हो; 8 का सही संदर्भ निर्धारित करें, यदि कोई हो; 9 शोधात्मक रूप से एक संदर्भ चुनें (यदि कोई हो) और संबंधित नियम लागू करें; 10 और फिर यदि और फिर 11 के साथ प्रतिस्थापित करें; 12 और फिर यदि और फिर 13 के साथ प्रतिस्थापित करें; 14 और फिर 15 शोधात्मक रूप से एक पूर्ववर्ती चुनें या; 16 के साथ या के साथ प्रतिस्थापित करें; 18 अंतिम फ़ंक्शन के लिए 17 अंत यदि इनपुट प्रमाण एक वृक्ष नहीं है (सामान्य रूप से, रिज़ॉल्यूशन ग्राफ हैं) इस मामले में, यह सुनिश्चित करने के लिए कि पुनर्लेखन नियम का एक आवेदन अन्य समाधान चरणों में हस्तक्षेप नहीं करने वाला है, एक सुरक्षित समाधान खंड द्वारा दर्शाए गए नोड की एक प्रति बनाना है। यह घोल सबूत के आकार को बढ़ाता है और ऐसा करते समय कुछ सावधानी बरतने की आवश्यकता होती है। एक अच्छा संपीड़न प्रदर्शन प्राप्त करने के लिए नियम चयन के लिए शोध महत्वपूर्ण है। सिमोन एट अल। नियमों के लिए वरीयता के निम्नलिखित क्रम का उपयोग करें (यदि दिए गए संदर्भ पर लागू हो): B2> B3> {B2 ', B1}> A1'> A2 (X> Y का अर्थ है कि X को Y पर प्राथमिकता दी जाती है)। प्रयोगों से पता चला है कि अकेले रिड्यूस एंड रिकंस्ट्रक्ट में एल्गोरिदम रीसाइकलपाइवट्स की तुलना में खराब संपीड़न/समय अनुपात है। हालांकि, जबकि रीसाइकल पाइवट्स को केवल एक बार प्रमाण पर लागू किया जा सकता है, एक बेहतर संपीड़न का उत्पादन करने के लिए कई बार रिड्यूस एंड रिकंस्ट्रक्ट लागू किया जा सकता है। रिड्यूस एंड रिकंस्ट्रक्ट और रीसाइकल पाइवट्स एल्गोरिदम को संयोजित करने के प्रयास से अच्छे परिणाम मिले हैं। छद्म कोड प्रमाण सिद्धांत के उदाहरण वाले लेखों पर टिप्पणी करें