1086 पेपर
यह शोध पत्र एपिस्टेमिक स्टेट रेप्लिकेशन (ESR) का प्रस्ताव करता है, जो एजेंटिक वितरित प्रणालियों के लिए एक नवीन ढांचा है जो पारंपरिक बिटवाइज़ स्टेट एग्रीमेंट को सिमेंटिक बिलीफ रेप्लिकेशन से बदल देता है, जिससे स्टोकेस्टिक एजेंट नियत स्टेट सिंक्रोनाइज़ेशन के बजाय संरचित साक्ष्य लॉग और सिमेंटिक अनुकूलता मेट्रिक्स के माध्यम से परिचालन निरंतरता बनाए रख सकते हैं।
यह शोध पत्र एक SMT-आधारित पाइपलाइन प्रस्तुत करता है जो समतलीय भूलभुलैया और त्रि-आयामी बुने हुए संरचनाओं के निर्माण के लिए स्कैफोल्ड (scaffolds) के रूप में कार्य करने हेतु इनपुट पैटर्न से स्व-परिहार (self-avoiding) या स्तरित पथों को संश्लेषित करता है।
यह शोध पत्र एब्स्ट्रैक्ट सिम्पलिसियल कॉम्प्लेक्स (abstract simplicial complexes) और स्टेलर सबडिवीजन (stellar subdivisions) का लीन (Lean) प्रूफ असिस्टेंट में पहला औपचारिक रूप प्रस्तुत करता है, जो एक विशुद्ध रूप से कॉम्बिनेटोरियल ढांचा प्रदान करता है जो मोर्फिज्म (morphisms), लिंक (links) और जॉइन्स (joins) जैसे ऑपरेशन्स को परिभाषित करता है, और उनके अंतर्संबंधों के संबंध में नई पहचान सिद्ध करता है, जिसमें मानक साहित्य से अनुपलब्ध परिणाम भी शामिल हैं।
इलेक्ट्रॉनिक प्रोसीडिंग्स इन थियोरेटिकल कंप्यूटर साइंस (EPTCS) का यह खंड 21वें इंटरनेशनल वर्कशॉप ऑन लॉजिकल फ्रेमवर्क्स एंड मेटा-लैंग्वेजेस: थ्योरी एंड प्रैक्टिस (LFMTP 2026) में प्रस्तुत योगदान दिए गए शोध पत्रों का संकलन है, जो FLoC 2026 सम्मेलन के अंतर्गत FSCD 2026 के एक उप-कार्यक्रम के रूप में 24 जुलाई, 2026 को लिस्बन, पुर्तगाल में आयोजित किया गया था।
यह शोध पत्र यह स्थापित करता है कि अधिकतम दो रैंक-चौड़ाई वाले परिमित ग्राफों के लिए, VR-पहचानने योग्यता (VR-recognizability) और काउंटिंग मोनैडिक सेकंड-ऑर्डर परिभाषितता (counting monadic second-order definability) एक समान हैं, जो स्प्लिट डिकंपोजिशन (split decompositions), पार्शियल-ट्री थ्योरी (partial-tree theory) और परिमित-अवस्था मूल्यांकन तकनीकों (finite-state evaluation techniques) का उपयोग करते हुए, सीमित रैखिक क्लीक-चौड़ाई (bounded linear clique-width) से ज्ञात समतुल्यता को पहले गैर-तुच्छ सीमित रैंक-चौड़ाई स्तर तक विस्तारित करता है।
यह शोध पत्र सिद्ध करता है कि प्रत्येक हेरेडिटरी ग्राफ क्लास (hereditary graph class) जो 2-वेल-क्वासी-ऑर्डर्ड (2-well-quasi-ordered) है, उसका क्लीक-विड्थ (clique-width) परिबद्ध है, जिससे पाउज़ेट के उस अनुमान की पुष्टि होती है कि सभी लेबल सेट्स के लिए 2-WQO, WQO के समतुल्य है और मोनैडिक डिपेंडेंस (monadic dependence) तथा बड़े वेल-लिंक्ड सेट्स (well-linked sets) के अपवर्जन के साथ एक संबंध स्थापित करते हुए इस परिणाम को स्थापित किया गया है।
यह शोधपत्र यह स्थापित करता है कि मोनाडिकली डिपेंडेंट (monadically dependent) ग्राफ वर्ग लगभग रैखिक पड़ोस जटिलता (almost linear neighborhood complexity) और का रेडियस-1 मर्ज-विड्थ (radius-1 merge-width) प्रदर्शित करते हैं, जो इन वर्गों के लिए पहला अपघटन-आधारित संरचनात्मक लक्षण वर्णन (decomposition-based structural characterization) और संगत निर्माण अनुक्रमों (construction sequences) की गणना के लिए एक कुशल एल्गोरिदम प्रदान करता है।
यह शोध पत्र लिनियराइज़ेबिलिटी (linearizability) के लिए लॉजिकल एटोमिटी (logical atomicity) की पूर्णता को सिद्ध करके आइरिस सेपरेशन लॉजिक (Iris separation logic) फ्रेमवर्क में एक खुले प्रश्न को हल करता है, जो यह प्रदर्शित करता है कि किसी भी लिनियराइज़ेबल डेटा स्ट्रक्चर को एक लॉजिकली एटोमिक स्पेसिफिकेशन असाइन किया जा सकता है और इस प्रकार विभिन्न लिनियराइज़ेबिलिटी प्रमाण तकनीकों के मशीनीकृत एकीकरण को सक्षम बनाया जा सकता है।
यह शोधपत्र सेपरेशन लॉजिक (separation logic) पर आधारित एक नवीन, लचीली रिफाइनमेंट तकनीक प्रस्तुत करता है जो अमूर्त मॉडलों (abstract models) और ठोस कोड (concrete code) के बीच ढीले जुड़ाव (loose coupling) के साथ कुशल समवर्ती कार्यान्वयन (concurrent implementations) के सत्यापन को सक्षम बनाकर मौजूदा पद्धतियों की सीमाओं को दूर करता है, जबकि यह सत्यापन लॉजिक और उपकरणों की एक विस्तृत श्रृंखला के साथ संगत बना रहता है।
यह शोध पत्र रस्ट (Rust) जैसी भाषाओं में साइड-इफेक्टफुल इटरेटर्स (side-effectful iterators) और उनके कंपोजिशन के मॉड्यूलर स्पेसिफिकेशन और वेरिफिकेशन के लिए एक नवीन कार्यप्रणाली प्रस्तुत करता है, जो संचित साइड-इफेक्ट्स (accumulated side effects) के बारे में तर्क करने की चुनौतियों और प्रूफ ऑटोमेशन को सक्षम करने के लिए इंडक्टिव इनवेरियंट्स (inductive invariants), हायर-ऑर्डर क्लोजर कॉन्ट्रैक्ट्स (higher-order closure contracts) और सेपरेशन लॉजिक (separation logic) का उपयोग करता है।