💻 computer science

Computing Witnesses Using the SCAN Algorithm

यह शोध पत्र द्वितीय-क्रम क्वांटिफायर एलिमिनेशन (second-order quantifier elimination) के लिए सैचुरेशन-आधारित SCAN एल्गोरिदम का विस्तार उन द्वितीय-क्रम क्वांटिफायर्स के लिए विटनेस (witnesses) की गणना करने हेतु करता है जो तार्किक रूप से समतुल्य प्रथम-क्रम सूत्रों (first-order formulas) को उत्पन्न करते हैं और इस विधि का एक प्रोटोटाइप कार्यान्वयन प्रस्तुत करता है।

मूल लेखक: Fabian Achammer, Stefan Hetzl, Renate A. Schmidt

प्रकाशित 2026-05-01

📖 5 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Fabian Achammer, Stefan Hetzl, Renate A. Schmidt

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आपके पास एक जटिल रेसिपी (एक तार्किक सूत्र/logical formula) है जिसमें एक गुप्त सामग्री शामिल है, जिसे हम "सामग्री X" (Ingredient X) कहते हैं। आप नहीं जानते कि "सामग्री X" क्या है, लेकिन आप जानते हैं कि यदि आप इसका कोई संस्करण उपयोग करते हैं, तो रेसिपी पूरी तरह से काम करती है।

समस्या:
आमतौर पर, जब तर्कशास्त्री (logicians) "सामग्री X" को हटाकर यह देखना चाहते हैं कि गुप्त सामग्री के बिना वास्तविक रेसिपी वास्तव में क्या है, तो वे सेकंड-ऑर्डर क्वांटिफायर एलिमिनेशन (SOQE) नामक एक विधि का उपयोग करते हैं। यह ऐसा है जैसे किसी अंतिम व्यंजन का वर्णन करना बिना उस गुप्त सामग्री का उल्लेख किए। कभी-कभी, आप इसे पूरी तरह से कर सकते हैं। लेकिन अक्सर, गणित कहता है, "हम परिणाम का वर्णन तो कर सकते हैं, लेकिन हम आपको यह नहीं बता सकते कि वह गुप्त सामग्री वास्तव में क्या थी।"

नई खोज (WSOQE):
यह शोध पत्र एक नए, अधिक महत्वाकांक्षी लक्ष्य को पेश करता है जिसे विटनेस्ड सेकंड-ऑर्डर क्वांटिफायर एलिमिनेशन (WSOQE) कहा जाता है। केवल अंतिम व्यंजन का वर्णन करने के बजाय, लेखक "सामग्री X" के लिए सटीक रेसिपी (जिसे "विटनेस" या गवाह कहा जाता है) खोजना चाहते हैं जो पूरे काम को सफल बनाती है। वे यह कहना चाहते हैं, "सामग्री X वास्तव में 'चीनी' है।"

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

यह शोध पत्र क्या जोड़ता है:
मूल SCAN रोबोट "सामग्री X" को हटाने और अंतिम परिणाम बताने में बहुत अच्छा था, लेकिन उसने यह जानकारी फेंक दी कि उसने यह कैसे किया। उसने "सामग्री X की रेसिपी" को सुरक्षित नहीं रखा।

लेखकों ने रोबोट को अपग्रेड किया है (इसे नया नाम WSCAN दिया गया है)। अब, जैसे ही रोबोट काम करता है, वह हर कदम का एक विस्तृत विवरण (डायरी) रखता है। अंत में, वह इस डायरी का उपयोग करके पीछे की ओर काम करता है और "सामग्री X" की सटीक रेसिपी को फिर से बनाता है।

वे इसे कैसे करते हैं ("डिटेक्टिव" उपमा):

सफाई (The Cleanup): रोबले सुरागों (clauses) के एक बिखरे हुए ढेर से शुरू करता है। यह "सामग्री X" को हटाने के लिए तार्किक चालें (जैसे पहेली सुलझाना) करता है।
डायरी (The Diary): जब भी रोबोट किसी सुराग को इसलिए हटा देता है क्योंकि अब उसकी आवश्यकता नहीं है, तो वह लिख देता है कि उसने उसे क्यों हटाया।
रिवर्स इंजीनियरिंग (The Reverse Engineering): एक बार जब रोबोट काम पूरा कर लेता है और "सामग्री X" हट जाती है, तो लेखक डायरी को देखते हैं। वे साफ परिणाम से वापस अस्त-व्यस्त शुरुआत की ओर काम करते हैं। रोबोट के चरणों के तर्क को उल्टा करके, वे एक ऐसा सूत्र बना सकते हैं जो बिल्कुल "सामग्री X" की तरह कार्य करता है।

"अनंत" बनाम "परिमित" (Infinite vs. Finite) समस्या:
कभी-कभी, जब रोबोट "सामग्री X" की रेसिपी खोजने की कोशिश करता है, तो रेसिपी अनंत रूप से लंबी हो जाती है (जैसे एक कहानी जो कभी खत्म नहीं होती)।

समाधान: लेखकों ने "एसाइक्लिक प्यूरिफिकेशन" (acyclic purification) नामक एक विशेष स्थिति खोजी है। एक ग्राफ की कल्पना करें जहाँ रोबोट की प्रक्रिया का प्रत्येक चरण एक नोड (node) है। यदि ग्राफ में कोई लूप (loops) नहीं हैं (यानी वह "एसाइक्लिक" है), तो "सामग्री X" की रेसिपी की गारंटी है कि वह छोटी और परिमित (finite) होगी। यदि लूप हैं, तो रेसिपी अनंत हो सकती है।
परिणाम: उन्होंने यह जांचने का एक तरीका बनाया है कि क्या प्रक्रिया लूप-मुक्त है। यदि यह लूप-मुक्त है, तो वे "सामग्री X" के लिए एक सरल, परिमित "फर्स्ट-ऑर्डर" रेसिपी बना सकते हैं। यदि यह नहीं है, तो वे अभी भी एक रेसिपी बना सकते हैं, लेकिन यह अनंत (या एक "फिक्स्पॉइंट" रेसिपी, जो एक शानदार तरीका है यह कहने का कि "एक ऐसी रेसिपी जो खुद को जारी रखने के लिए स्वयं को संदर्भित करती है") हो सकती है।

उल्लेखित वास्तविक दुनिया के उदाहरण:
यह शोध पत्र केवल सिद्धांत की बात नहीं करता है; उन्होंने इसे 44 अलग-अलग तार्किक पहेलियों पर परखा।

ग्राफ रीचेबिलिटी (Graph Reachability): उन्होंने इसका उपयोग एक मानचित्र में नेविगेट करने के बारे में समस्या को हल करने के लिए किया। कल्पना कीजिए कि आपके पास शहरों और सड़कों का एक मानचित्र है, और आप यह जानना चाहते हैं कि सिटी A से शुरू करके आप किन शहरों तक पहुँच सकते हैं बिना सिटी B से टकराए। रोबोट ने सफलतापूर्वक उस सटीक नियम (विटनेस) को खोजा जो यह परिभाषित करता है कि कौन से शहर सुरक्षित रूप से जाने योग्य हैं।
समानता (Equality): उन्होंने दिखाया कि उनका रोबोट उन नियमों को भी संभाल सकता है जहाँ चीजें "बराबर" (जैसे $a = b$ ) होती हैं, जो पहेली को कठिन बनाता है, लेकिन रोबोट फिर भी गुप्त सामग्री की रेसिपी खोजने में सक्षम रहता है।

मुख्य निष्कर्ष (The Bottom Line):
यह शोध पत्र एक मौजूदा लॉजिक टूल (SCAN) को लेता है जो अज्ञात चरों (variables) को हटाने में अच्छा था और उसे अपग्रेड करता है ताकि वह न केवल उन्हें हटाए बल्कि यह भी प्रकट करे कि वे वास्तव में क्या थे। यह "समाधान खोजने" और "अज्ञात की विशिष्ट परिभाषा खोजने" के बीच के अंतर को पाटता है, जो एक प्रोटोटाइप कार्यान्वयन प्रदान करता है जो वास्तविक उदाहरणों पर काम करता है, हालांकि यह स्वीकार करता है कि कभी-कभी, अज्ञात के लिए "रेसिपी" इतनी जटिल हो सकती है कि उसे एक एकल वाक्य में लिखना संभव न हो।

यहाँ फैबियन अचरमर, स्टीफन हेत्ज़ल और रेनेट ए. श्मिट के शोध पत्र "Computing Witnesses Using the SCAN Algorithm" का विस्तृत तकनीकी सारांश दिया गया है।

1. समस्या विवरण (Problem Statement)

यह शोध पत्र सेकंड-ऑर्डर क्वांटिफायर एलिमिनेशन (SOQE) को संबोधित करता है, जो एक दिए गए सेकंड-ऑर्डर फॉर्मूला $\exists X \phi$ (जहाँ $\phi$ फर्स्ट-ऑर्डर है) के लिए एक तार्किक रूप से समतुल्य फर्स्ट-ऑर्डर फॉर्मूला $\psi$ खोजने की समस्या है। जबकि सामान्य रूप से SOQE अनिर्णयकारी (undecidable) है, विशिष्ट उप-वर्गों (subclasses) के लिए व्यावहारिक एल्गोरिदम मौजूद हैं।

लेखक एक अधिक सामान्य समस्या प्रस्तुत करते हैं जिसे विटनेस्ड सेकंड-ऑर्डर क्वांटिफायर एलिमिनेशन (WSOQE) कहा जाता है। केवल एक समतुल्य फर्स्ट-ऑर्डर फॉर्मूला खोजने के बजाय, लक्ष्य एक विटनेस (witness) खोजना है: फर्स्ट-ऑर्डर प्रेडिकेट्स का एक टुपल $\alpha$ ताकि:
$\exists X \phi \equiv \phi[X \leftarrow \alpha]$
इसका अर्थ है कि सेकंड-ऑर्डर फॉर्मूला उस फर्स्ट-ऑर्डर फॉर्मूला के समतुल्य है जो प्रेडिकेट वेरिएबल्स $X$ को विशिष्ट फर्स्ट-ऑर्डर डेफिनिशन $\alpha$ के साथ प्रतिस्थापित (substitute) करके प्राप्त किया जाता है।

WSOQE का महत्व:

यह SOQE और फॉर्मूला इक्वेशन्स (FEQ) (एक $\alpha$ खोजना जिससे $\models \phi[X \leftarrow \alpha]$ हो) के बीच के अंतर को पाटता है।
यह नॉलेज रिप्रेजेंटेशन (forgetting/projection), मोडल कॉरेस्पोंडेंस थ्योरी और प्रोग्राम वेरिफिकेशन (लूप इनवेरिएंट्स खोजना) में अनुप्रयोगों के लिए अत्यंत महत्वपूर्ण है।
मानक SOQE के विपरीत, जो केवल परिणाम देता है, WSOQE एलिमिनेट किए गए प्रेडिकेट्स की डेफिनेशन प्रदान करता है, जिससे नॉलेज बेस की संरचना सुरक्षित रहती है।

2. कार्यप्रणाली: WSCAN एल्गोरिदम (Methodology: The WSCAN Algorithm)

लेखक WSCAN प्रस्तावित करते हैं, जो मौजूदा SCAN एल्गोरिदम (SOQE के लिए एक सैचुरेशन-आधारित थ्योरम प्रूवर) का एक विस्तार है। मुख्य कार्यप्रणाली में दो मुख्य चरण शामिल हैं:

A. SCAN डेरिवेशन (The SCAN Derivation)

एल्गोरिदम क्लॉज सेट्स (clause sets) पर कार्य करता है। यह इनपुट फॉर्मूला को क्लॉज़ल नॉर्मल फॉर्म में बदलता है और एक विशिष्ट इन्फरेंस कैलकुलस $\mathcal{I}$ का उपयोग करके सैचुरेशन प्रक्रिया करता है:

कॉन्स्ट्रेंट रेज़ोल्यूशन और फैक्टरिंग (Constraint Resolution & Factoring): मानक यूनिफिकेशन के बजाय, ये नियम टर्म्स के बीच असमानता बाधाओं (inequality constraints) (जैसे, $t \not\simeq t'$ ) को पेश करते हैं।
कॉन्स्ट्रेंट एलिमिनेशन (Constraint Elimination): बाधाओं को हटाने के लिए टर्म्स को यूनिफाई करता है।
डिलीशन रूल्स (Deletion Rules):
- एक्सटेंडेड प्योरिटी डिलीशन (Extended Purity Deletion): उन क्लॉज़ों को हटाता है जिनमें $X$ है यदि $X$ केवल एक पोलरिटी (सभी पॉजिटिव या सभी नेगेटिव) के साथ आता है।
- प्यूरीफाइड क्लॉज़ डिलीशन (Purified Clause Deletion): एक क्लॉज़ $P$ को (जिसमें $X$ है) हटाता है यदि "पर्याप्त संख्या में" इन्फरेंस किए जा चुके हैं जिससे शेष क्लॉज़ सेट $P$ के रेज़ोल्यूशन क्लोजर को तार्किक रूप से सिद्ध करता है। इसे वेरिएबल एलिमिनेशन और सबसमप्शन (subsumption) का उपयोग करते हुए एक फॉरवर्ड रेडंडेंसी मानदंड के माध्यम से औपचारिक रूप दिया गया है।

यह प्रक्रिया तब तक जारी रहती है जब तक कि सभी $X$ -लिटरेल्स को हटा नहीं दिया जाता, जिसके परिणामस्वरूप $\exists X N$ के समतुल्य एक फर्स्ट-ऑर्डर क्लॉज़ सेट $N^*$ प्राप्त होता है।

B. विटनेस कंस्ट्रक्शन (नीचे से ऊपर की ओर) (Witness Construction - Bottom-Up)

नया योगदान डेरिवेशन हिस्ट्री से एक विटनेस $\sigma$ को निकालना है। एल्गोरिदम विटनेस को पीछे की ओर (अंतिम अवस्था से प्रारंभिक अवस्था की ओर) निर्मित करता है:

बेस केस: यदि अंतिम क्लॉज़ सेट $N_m$ में कोई $X$ नहीं है, तो आइडेंटिटी सब्स्टीट्यूशन एक विटनेस है।
इंडक्टिव स्टेप: प्रत्येक डेरिवेशन स्टेप $S_i$ $S_{i}$ के लिए जो $N_{i-1}$ $N_{i - 1}$ को $N_i$ $N_{i}$ में बदलता है, एल्गोरिदम एक सब्स्टीट्यूशन $\tau_{S_i}$ $τ_{S_{i}}$ की गणना करता है ताकि यदि $\sigma_i$ $σ_{i}$ के लिए $N_i$ $N_{i}$ एक विटनेस है, तो $\tau_{S_i}\sigma_i$ $τ_{S_{i}} σ_{i}$ के लिए $N_{i-1}$ $N_{i - 1}$ एक विटनेस हो।
- मानक इन्फरेंस स्टेप्स (रेज़ोल्यूशन, फैक्टरिंग, आदि) के लिए, $\tau$ आइडेंटिटी है।
- एक्सटेंडेड प्योरिटी डिलीशन के लिए, $\tau$ पोलरिटी के आधार पर $X$ को $\top$ या $\bot$ पर सेट करता है।
- प्यूरीफाइड क्लॉज़ डिलीशन (जटिल मामला) के लिए, एल्गोरिदम हटाए गए क्लॉज़ के लोकल रेज़ोल्यूशन क्लोजर के आधार पर एक विटनेस निर्मित करता है।

C. अनंत विटनेस को संभालना (Handling Infinite Witnesses)

प्यूरीफाइड क्लॉज़ों के लिए उपयोग किया जाने वाला रेज़ोल्यूशन क्लोजर अनंत हो सकता है, जिससे अनंत विटनेस (अनंत कंजंक्शन्स के रूप में व्यक्त) उत्पन्न हो सकते हैं। शोध पत्र दो समाधान पेश करता है:

फिक्स्टपॉइंट विटनेस (Fixpoint Witnesses): अनंत विटनेस को फिक्स्टपॉइंट लॉजिक में एक ग्रेटेस्ट फिक्स्टपॉइंट ($gfp$) के रूप में व्यक्त किया जाता है। यह संभावित रूप से अनंत परिभाषा के लिए एक परिमित प्रतिनिधित्व प्रदान करता है।
फर्स्ट-ऑर्डर विटनेस (एसाइक्लिक कंडीशन) (First-Order Witnesses - Acyclic Condition): लेखक एक स्थिति परिभाषित करते हैं जिसे $k$ -एसाइक्लिकली प्यूरीफाइड कहा जाता है। यदि डिलीशन स्टेप से जुड़ा "प्यूरीफिकेशन सबसमप्शन ग्राफ" एसाइक्लिक है, तो विटनेस को रेज़ोल्यूशन क्लोजर के एक बाउंडेड इटरेशन का उपयोग करके एक परिमित, फर्स्ट-ऑर्डर प्रेडिकेट के रूप में कंप्यूट किया जा सकता है।

3. मुख्य योगदान (Key Contributions)

WSCAN एल्गोरिदम: क्लॉज़ सेट्स पर SOQE के लिए विटनेस कंप्यूट करने के लिए एक पूर्ण विधि, जो SCAN एल्गोरिदम का विस्तार है।
करेक्टनेस प्रूफ (Correctness Proofs):
- यह प्रमाण कि निर्मित सब्स्टीट्यूशन $\sigma$ एक वैध विटनेस है ( $\exists X N \equiv N\sigma$ )।
- मूल SCAN एल्गोरिदम के लिए एक नया करेक्टनेस प्रूफ जो विटनेस कंस्ट्रक्शन लॉजिक से व्युत्पन्न है।
फर्स्ट-ऑर्डर विटनेस गारंटी: एसाइक्लिक प्यूरीफिकेशन स्थिति की पहचान, जो यह गारंटी देती है कि परिणामी विटनेस एक फर्स्ट-ऑर्डर फॉर्मूला है (अनंत या फिक्स्टपॉइंट एक्सप्रेशन से बचते हुए)।
एकमैन के लेम्मा का विस्तार (Extension of Ackermann's Lemma): लेखक सिद्ध करते हैं कि उनकी विधि एकमैन के लेम्मा (SOQE के लिए एक क्लासिक विधि) को समाहित करती है और इसे मिश्रित पोलरिटी वाले मामलों तक विस्तारित करती है।
बैकग्राउंड थ्योरीज को संभालना: विधि को समानता तर्क (पैरामोड्यूलेशन के माध्यम से) और फर्स्ट-ऑर्डर बैकग्राउंड थ्योरीज को संभालने के लिए विस्तारित किया गया है, जिससे ग्राफ रीचेबिलिटी समस्याओं और अन्य कंस्ट्रेंड हॉर्न क्लॉज़ समस्याओं को हल करना संभव होता है।
प्रोटोटाइप इम्प्लीमेंटेशन: GAPT (जनरल आर्किटेक्चर फॉर प्रूफ थ्योरी) सॉफ्टवेयर पैकेज (वर्जन 2.19.0) में एक प्रोटोटाइप कार्यान्वयन।

4. परिणाम और मूल्यांकन (Results and Evaluation)

कार्यान्वयन: प्रोटोटाइप का परीक्षण 44 उदाहरणों (साहित्य और कस्टम) पर किया गया।
प्रदर्शन:
- 10-सेकंड के टाइमआउट के भीतर 90.9% उदाहरणों (44 में से 40) के लिए SCAN डेरिवेशन पाए गए।
- विटनेस कंप्यूटेशन डेरिवेशन खोजने (औसत 375 ms) की तुलना में अत्यंत तेज़ था (औसत 0.619 ms)।
- विटनेस का आकार आम तौर पर छोटा था (औसत 6.9 सिम्बल्स)।
क्षमताएं: सिस्टम ने सफलतापूर्वक उन डेरिवेशनों के लिए फर्स्ट-ऑर्डर विटनेस कंप्यूट किए जो पहले अनंत विटनेस देते थे या जिन्हें फिक्स्टपॉइंट लॉजिक की आवश्यकता थी, विशेष रूप से एसाइक्लिक प्यूरीफिकेशन ग्राफ वाले मामलों में।
सीमाएं:
- विधि के लिए इनपुट क्लॉज़ सेट (यूनिवर्सली क्वांटिफाइड डोमेन वेरिएबल्स) होना आवश्यक है।
- यह उन मामलों को नहीं संभाल सकती जहाँ स्किमोलिज़ेशन (Skolemization) की आवश्यकता होती है और उसे रिवर्स नहीं किया जा सकता (जैसे, $\exists X \exists u \exists v (X(u) \land \neg X(v))$ ), क्योंकि परिणामी विटनेस में मूल भाषा में मौजूद न होने वाले स्किमोल कॉन्स्टेंट्स होंगे।
- डेरिवेशन के लिए सर्च स्पेस बड़ा हो सकता; वर्तमान कार्यान्वयन बैकट्रैकिंग का उपयोग करता है लेकिन विशाल क्लॉज़ सेट्स के लिए अनुकूलित नहीं है।

5. महत्व (Significance)

यह कार्य महत्वपूर्ण है क्योंकि यह SCAN एल्गोरिदम को केवल क्वांटिफायर एलिमिनेट करने वाले उपकरण से बदलकर एलिमिनेट किए गए प्रेडिकेट्स की परिभाषाओं को सिंथेसाइज़ करने वाले उपकरण में बदल देता है।

सैद्धांतिक सेतु (Theoretical Bridge): यह सेकंड-ऑर्डर क्वांटिफायर एलिमिनेशन (SOQE) और फॉर्मूला इक्वेशन्स (FEQ) के क्षेत्रों को एकीकृत करता है, यह दिखाते हुए कि वे एक ही सिक्के के दो पहलू हैं।
व्यावहारिक अनुप्रयोग: स्पष्ट फर्स्ट-ऑर्डर डेफिनिशन (विटनेस) प्रदान करके, यह विधि सीधे तौर पर निम्नलिखित के लिए लागू है:
- नॉलेज रिप्रेजेंटेशन: नॉलेज स्ट्रक्चर को बनाए रखते हुए यूनिफॉर्म इंटरपोलेन्ट्स और फॉरगेटिंग प्रेडिकेट्स बनाना।
- वेरिफिकेशन: प्रोग्राम वेरिफिकेशन (कंस्ट्रेंड हॉर्न क्लॉज़ को हल करना) के लिए लूप इनवेरिएंट्स को स्वचालित रूप से जेनरेट करना।
- मोडल लॉजिक: मोडल लॉजिक के लिए कॉरेस्पोंडेंस एक्सिओम्स को कंप्यूट करना।

यह पेपर स्थापित करता है कि व्यापक वर्ग के डेरिवेशंस (वे जिनमें एसाइक्लिक प्यूरीफिकेशन ग्राफ है) के लिए, जटिल सेकंड-ऑर्डर समस्या को एक परिमित, फर्स्ट-ऑर्डर विटनेस खोजने में बदला जा सकता है, जो स्वचालित तर्क (automated reasoning) के लिए एक शक्तिशाली नया उपकरण प्रदान करता है।