A Strategy Language for Controlled Proof Search

तकनीकी सारांश: नियंत्रित प्रमाण खोज के लिए एक रणनीति भाषा

समस्या विवरण
स्वचालित तर्क (automated reasoning) में, किसी तार्किक गणना की स्थिर पूर्णता (किसी प्रमेय के लिए प्रमाण का अस्तित्व) यह गारंटी नहीं देती कि एक प्रवर (prover) गतिशील रूप से पूर्ण होगा (प्रमाण खोजने की क्षमता)। अर्ध-निर्णय योग्य (semi-decidable) तर्कशास्त्रों में, निष्कर्ष नियम (inference rules) अनंत उत्तराधिकारी उत्पन्न कर सकते हैं। यदि प्रमाण खोज रणनीति अनुचित अन्वेषण (unfair exploration) का उपयोग करती है—जैसे कि एक सहज डेप्थ-फर्स्ट दृष्टिकोण जो अनिश्चित काल के लिए एक ही शाखा को प्राथमिकता देता है—तो वह प्रासंगिक निष्कर्षों को हमेशा के लिए स्थगित कर सकती है, जिससे वैध प्रमाणों की खोज करने में विफल हो सकती है भले वे मौजूद हों। यह समस्या Pgeon जैसे ढांचों में विशेष रूप से गंभीर है, जो निष्कर्ष नियमों को प्रमाण-खोज रणनीतियों से अलग करते हैं, क्योंकि अन्वेषण नीति का डिज़ाइन सफलता का एक महत्वपूर्ण निर्धारक बन जाता है।

कार्यप्रणाली
यह शोध पत्र Pgeon के लिए एक औपचारिक रणनीति भाषा प्रस्तुत करता है, जो एक मेटा-प्रवर ढांचा है और तार्किक गणनाओं के घोषणात्मक विनिर्देशों (declarative specifications) को निष्पादन योग्य प्रोवर्स में संकलित करता है। मुख्य पद्धतिगत परिवर्तन प्रमाण खोज को अवस्थाओं (states) के बीच एक संबंध के रूप में नहीं, बल्कि स्ट्रीम्स (streams) के माध्यम से प्रमाण अवस्थाओं के प्रगणना (enumeration) के रूप में मॉडल करना है।

1. औपचारिक अर्थशास्त्र (Formal Semantics): एक प्रमाण अवस्था ($\Sigma$) को आंशिक रूप से निर्मित प्रमाण वृक्ष के रूप में माना जाता है। एक रणनीति को एक फलन $s: \Sigma \to \text{Str}(\Sigma)$ के रूप में परिभाषित किया गया है, जो एक अवस्था को उत्तराधिकारी अवस्थाओं की एक स्ट्रीम (परिमित या अनंत) में मैप करता है। यह गैर-निश्चयात्मकता (non-determinism) को स्पष्ट बनाता है:

   • एक खाली स्ट्रीम विफलता का प्रतिनिधित्व करती है।
   • एक एकल (singleton) स्ट्रीम निश्चयात्मक सफलता का प्रतिनिधित्व करती है।
   • कई तत्वों वाली एक स्ट्रीम गैर-निश्चयात्मक शाखाकरण (branching) का प्रतिनिधित्व करती है।
   • अनंत स्ट्रीम उन नियमों का प्रतिनिधित्व करती है जो अनियंत्रित संख्या में उत्तराधिकारी उत्पन्न कर सकते हैं।

2. संयोजक (Combinators): भाषा इन रणनीतियों को संयोजित करने के लिए ऑपरेटरों का एक सेट प्रदान करती है, जो पक्षपाती (depth-first) और निष्पक्ष (interleaved) अन्वेषण के बीच अंतर करती है:

   • अनुक्रमिक संयोजन (Sequential Composition - $;$): एक अन्य के परिणामों पर एक रणनीति लागू करता है।
   • बायां-पक्षपाती चयन (Left-biased Choice - $\parallel$): पहली रणनीति का प्रयास करता है; यदि यह विफल (खाली स्ट्रीम) हो जाती है, तो यह दूसरी रणनीति पर वापस आता है।
   • निष्पक्ष अनुक्रमिक संयोजन (Fair Sequential Composition - $\&;$): विकर्णीकरण (diagonalization - $\triangle$) का उपयोग करके अनुक्रमिक अनुप्रयोगों के परिणामों को इंटरलीव करता है, यह सुनिश्चित करते हुए कि यदि कोई परिणाम परिमित चरणों में सुलभ है, तो उसे अंततः खोजा जाएगा।
   • निष्पक्ष चयन (Fair Choice - $\&|$): दो वैकल्पिक रणनीतियों के परिणामों को निष्पक्ष रूप से इंटरलीव करता है।
   • पुनरावृत्ति (Repetition - $*$): इसे निष्पक्ष अनुक्रमिक संयोजन ($\mu X. \text{id} \&; (s \&; X)$) का उपयोग करके न्यूनतम फिक्स्डपॉइंट (least fixpoint) के रूप में परिभाषित किया गया है, जो यह सुनिश्चित करता है कि सभी परिमित पुनरावृत्ति गहराइयों को खोजा जाए, न कि केवल सख्त डेप्थ-फर्स्ट तरीके से आगे बढ़े।

3. प्राथमिक संचालन (Primitive Operations): भाषा में प्राथमिक नियम ($r$) और एक व्यापक अनुप्रयोग ऑपरेटर ($r!$) शामिल है जो एक अवस्था में सभी स्वीकार्य मिलानों पर नियम लागू करता है।

प्रमुख योगदान

• संयोजन योग्य स्ट्रीम अर्थशास्त्र (Compositional Stream Semantics): यह शोध पत्र ऐसे रणनीति संयोजकों के लिए एक संयोजन योग्य बीजगणित प्रदान करता है जहाँ खोज स्थान को एक प्रथम-श्रेणी की वस्तु (एक स्ट्रीम) के रूप में पुनर्रूपित किया जाता है। यह स्टैक अनुशासन या निरंतरता (continuations) जैसे कार्यान्वयन विवरणों से स्वतंत्र होकर निष्पक्षता और प्रगणना के बारे में तर्क करने की अनुमति देता है।
• निष्पक्षता तंत्र (Fairness Mechanisms): विकर्णीकरण-आधारित इंटरलीविंग ऑपरेटरों ($\&;$ और $\&|$) को पेश करके, यह ढांचा "भुखमरी" (starvation) की समस्या को संबोधित करता है जहाँ अनंत शाखाएं परिमित प्रमाणों की खोज को रोक देती हैं।
• Pgeon के लिए औपचारिक रणनीति भाषा: यह कार्य Pgeon ढांचे के रणनीति घटक को औपचारिक रूप देता है, जो प्रमाण खोज के नियंत्रण प्रवाह को एक घोषणात्मक भाषा में अमूर्त (abstract) करता है।

परिणाम और केस स्टडीज
शोध पत्र दो केस स्टडीज के माध्यम से इस दृष्टिकोण की अभिव्यक्ति और प्रभावशीलता को प्रदर्शित करता है:

1. प्रथम-क्रम तर्क (First-Order Logic - LK): लेखक क्लोजर (unification) और नियम संतृप्ति (rule saturation) के बीच परस्पर क्रिया को संबोधित करते हैं। एक सहज रणनीति अक्सर प्रमाण खोजने में विफल रहती है क्योंकि यह बहुत जल्दी विशिष्ट इंस्टांशिएशन (instantiation) के प्रति प्रतिबद्ध हो जाती है। प्रस्तावित रणनीति, $(\odot^* \&; (\alpha \parallel \delta \parallel \beta \parallel \gamma!)^*)^*$, क्लोजर प्रयासों को नियम संतृप्ति के साथ इंटरलीव करने के लिए निष्पक्ष संयोजन का उपयोग करती है। यह सुनिश्चित करता है कि विभिन्न यूनिफिकेशन विकल्पों को सभी खोज गहराइयों में खोजा जाए, जिससे सिस्टम को एक क्लोजिंग डेरिवेशन को मिस करते हुए अनंत इंस्टांशिएशन लूप में फंसने से रोका जा सके।

2. मोडल लॉजिक (Modal Logic - S4): S4 में, $\theta$ (सूत्रों का मनमाना निष्कासन) गैर-निश्चयात्मक नियम है जो S4 को सक्षम करने के लिए आवश्यक है, लेकिन यह उन सूत्रों को हटाने का जोखिम उठाता है जो क्लोजर के लिए आवश्यक हैं। $\theta$ का अनियंत्रित उपयोग मृत अंत (dead ends) की ओर ले जाता है। लेखक एक संयुक्त रणनीति $\theta^* \&; \text{S4}$ का प्रस्ताव करते हैं, जो S4 अनुप्रयोगों को सक्षम करने के लिए सूत्रों को हटाने के सभी तरीकों का निष्पक्षता से अन्वेषण करती है। इसे एक बड़े रणनीति $((\alpha \parallel \beta \parallel T)^*; (\theta^* \&; \text{S4}))^*$ में एकीकृत किया गया है, यह सुनिश्चित करते हुए कि यदि S4 के सफल अनुप्रयोग के लिए हटाए गए सूत्रों के विशिष्ट उपसमूह की आवश्यकता है, तो वह कॉन्फ़िगरेशन भुखमरी के बिना अंततः प्राप्त हो जाएगा।

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