Proof compression
प्रमाण सिद्धांत में, गणितीय तर्क का एक क्षेत्र, प्रमाण संपीड़न औपचारिक प्रमाणों को एल्गोरिथम रूप से संपीड़ित करने की समस्या है। विकसित एल्गोरिदम का उपयोग एस. ए. टी. सॉल्वर, एस. एम. टी.-सॉल्वर, फर्स्ट-ऑर्डर थ्योरम प्रोवर और प्रूफ असिस्टेंट जैसे स्वचालित प्रमेय साबित करने वाले उपकरणों द्वारा उत्पन्न प्रमाणों को बेहतर बनाने के लिए किया जा सकता है। समस्या प्रतिनिधित्व प्रस्तावात्मक तर्क में खंड सी के एक समूह से एक खंड का एक संकल्प प्रमाण एक निर्देशित चक्रीय ग्राफ (डीएजी) हैः इनपुट नोड्स स्वयंसिद्ध निष्कर्ष (परिसर के बिना) हैं जिनके निष्कर्ष सी के तत्व हैं, संकल्प नोड्स संकल्प निष्कर्ष हैं, और प्रमाण में निष्कर्ष के साथ एक नोड है। डी. ए. जी. में एक नोड से एक नोड तक का किनारा होता है यदि और केवल तभी जब इसका एक आधार इसका निष्कर्ष हो। इस मामले में, एक बच्चा है, और एक माता-पिता है। एक नोड जिसमें कोई बच्चे नहीं हैं, एक मूल है। एक प्रमाण संपीड़न एल्गोरिथ्म कम नोड्स के साथ एक नया डी. ए. जी. बनाने की कोशिश करेगा जो एक वैध प्रमाण का प्रतिनिधित्व करता है या, कुछ मामलों में, एक उपसमुच्चय का एक वैध प्रमाण। एक सरल उदाहरण आइए क्लॉज के सेट से क्लॉज के लिए एक संकल्प प्रमाण लें यहाँ हम देख सकते हैंः और इनपुट नोड्स हैं। नोड में एक धुरी होती है, बाएं हल किए गए शाब्दिक दाएं हल किए गए शाब्दिक निष्कर्ष यह है कि खंड परिसर नोड्स का निष्कर्ष है और (इसके माता-पिता) डी. ए. जी. होगा और इसके माता-पिता हैं और यह प्रमाण ए का मूल है (संकल्प) सी का खंडन सी से एक संकल्प प्रमाण है। यह एक सामान्य दिया गया नोड है, खंड या खंड का उल्लेख करने के लिए जिसका अर्थ है निष्कर्ष खंड, और (उप) प्रमाण जिसका अर्थ है (उप) प्रमाण जिसका एकमात्र मूल है। कुछ कार्यों में संकल्प निष्कर्षों का एक बीजगणितीय प्रतिनिधित्व पाया जा सकता है। धुरी के और साथ के रिज़ॉल्वेंट को के रूप में दर्शाया जा सकता है। जब धुरी विशिष्ट रूप से परिभाषित या अप्रासंगिक होती है, तो हम इसे छोड़ देते हैं और सरलता से लिखते हैं। इस तरह, खंडों के समूह को एक कम्यूटेटिव ऑपरेटर के साथ एक बीजगणित के रूप में देखा जा सकता है; और संबंधित शब्द बीजगणित में शब्द एक संकेतन शैली में संकल्प प्रमाण को दर्शाते हैं जो सामान्य ग्राफ संकेतन की तुलना में संकल्प प्रमाण का वर्णन करने के लिए अधिक संक्षिप्त और अधिक सुविधाजनक है। हमारे अंतिम उदाहरण में डी. ए. जी. का संकेतन होगा या बस हम पहचान सकते हैं। कम्प्रेशन एल्गोरिदम क्रमिक कलन प्रमाणों के संपीड़न के लिए एल्गोरिदम में कट परिचय और कट उन्मूलन शामिल हैं। प्रस्तावात्मक संकल्प प्रमाणों के संपीड़न के लिए एल्गोरिदम में रीसाइकल यूनिट, रीसाइकल पाइवट्स, रीसाइकल पाइवट्स, इंटरसेक्शन, लोअर यूनिट, लोअर यूनिवल्स, स्प्लिट, रिड्यूस एंड रिकंस्ट्रक्ट और सबसमप्शन शामिल हैं। नोट्स सबूत सिद्धांत