1086 पेपर
यह शोध पत्र यह स्थापित करता है कि 3-आयामी स्टेट्स के साथ वेक्टर एडिशन सिस्टम (3-VASS) के लिए रीचेबिलिटी समस्या (reachability problem) एक पदानुक्रमित पंपेबिलिटी विश्लेषण (hierarchical pumpability analysis) के माध्यम से सबसे छोटे रन के लिए डबली-एक्सपोनेंशियल लंबाई की सीमा को सिद्ध करके EXPSPACE में है, जिससे पूर्व में ज्ञात 2-EXPSPACE ऊपरी सीमा में सुधार हुआ है।
यह शोध पत्र Rocq प्रूफ असिस्टेंट में DPLL SAT-सॉल्विंग प्रक्रिया के लिए एक अमूर्त, नियम-आधारित ट्रांज़िशन सिस्टम का औपचारिक सत्यापन प्रस्तुत करता है, जो शुद्ध लिटरल (pure literal) नियम के साथ इसका विस्तार करते हुए इसकी शुद्धता, पूर्णता और समाप्ति को स्थापित करता है और एक सत्यापित अमूर्त रणनीति से एक ठोस समाप्त होने वाले सॉल्वर को व्युत्पन्न करता है।
यह शोध पत्र रैंडम ग्राफ थ्योरी को अनुभवजन्य डेटा के साथ एकीकृत करके यथार्थवादी बड़े लेबल वाले ट्रांज़िशन सिस्टम उत्पन्न करने के लिए एक संभाव्य मॉडल प्रस्तावित करता है, यह प्रदर्शित करते हुए कि ये सिस्टम जैसे-जैसे इनका आकार अनंत की ओर बढ़ता है, LTL और CTL गुणों के लिए अभिसरण (convergence) या 0-1 नियम प्रदर्शित करते हैं, साथ ही इन साहसिक सीमाओं (asymptotic limits) को निर्धारित करने के लिए एल्गोरिदम भी प्रदान करता है।
यह शोध पत्र डिसइंटीग्रेशन टेम्पोरल लॉजिक (DTL) प्रस्तुत करता है, जो मेजर डिसइंटीग्रेशन पर आधारित एक नया संभाव्य टेम्पोरल लॉजिक है जो संभाव्य गैर-हस्तक्षेप (probabilistic non-interference) जैसे जटिल हाइपरप्रॉपर्टीज को व्यक्त करता है, और पूर्ण लॉजिक की अनिश्चितता (undecidability) के बावजूद दो निर्णय योग्य खंडों (decidable fragments) की पहचान करता है जिनमें कुशल मॉडल-चेकिंग प्रक्रियाएं मौजूद हैं।
यह शोध पत्र क्यूबिकल एगडा (Cubical Agda) में एक रचनात्मक औपचारिकीकरण प्रस्तुत करता है जो पूर्ण बेयसियन कंडीशनिंग (Bayesian conditioning) के लिए मानक उत्तल-बीजगणितीय विनिमय अभिगृहीत (convex-algebra interchange axiom) की अपर्याप्तता को पहचानता है, परिणामी संरचनात्मक बेमेल को हल करने के लिए एक न्यूनतम सामान्यीकरण का प्रस्ताव करता है, और एक अमूर्त क्रमबद्ध-क्षेत्र इंटरफ़ेस (ordered-field interface) पर पर्ल के डी-सेपरेशन प्रमेय (Pearl's d-separation theorem) और संबंधित संभाव्यता अभिगृहीतों की सुदृढ़ता को सत्यापित करता है।
यह शोधपत्र 21वें इंटरनेशनल वर्कशॉप ऑन टर्मिनेशन (WST 2026) के कार्यवाही विवरण प्रस्तुत करता है, जो फेडरेटेड लॉजिक कॉन्फ्रेंस (FLoC 2026) के भीतर 13वीं इंटरनेशनल जॉइंट कॉन्फ्रेंस ऑन ऑटोमेटेड रीजनिंग (IJCAR 2026) के एक उप-इवेंट के रूप में 25 जुलाई, 2026 को लिस्बन में आयोजित किया गया था।
यह शोध पत्र "इंटरवेंशनल ग्राउंडिंग ऑडिट्स" (interventional grounding audits) को प्रस्तुत करता है, जो एक ब्लैक-बॉक्स विधि है जो नए प्रतीकों के साथ आधारों (premises) को प्रतिस्थापित करके लार्ज लैंग्वेज मॉडल की चेन-ऑफ-थॉट रीजनिंग की तार्किक निर्भरता को मान्य करती है, और प्रोंटोक्यूए (ProntoQA) बेंचमार्क पर सेल्फ-कंसिस्टेंसी बेसलाइन की तुलना में "सही उत्तर, गलत तर्क" वाली खामियों का पता लगाने की अपनी श्रेष्ठ क्षमता प्रदर्शित करती है।
यह शोधपत्र अंतराल संरचनाओं (interval structures) पर आधारित एक एकीकृत अर्थपूर्ण ढांचे (unified semantic framework) को प्रस्तुत करता है जो परिचालन अर्थों (operational semantics) को स्वतंत्र रणनीतियों में विभाजित करता है ताकि विविध प्रतिक्रिया प्रणाली वेरिएंट्स (reaction system variants) को समाहित किया जा सके और पेट्री नेट्स (Petri nets) जैसे अन्य कम्प्यूटेशनल मॉडलों तक इसका विस्तार किया जा सके, जिससे कम्प्यूटेशनल औपचारिकताओं (computational formalisms) के विश्लेषण और विकास के लिए एक सामान्य आधार प्रदान किया जा सके।
यह शोध पत्र क्वांटम ऑर्केस्ट्रा मोनाड के भीतर पुनरावर्ती हाइब्रिड क्वांटम प्रोग्रामों के लिए एक श्रेणीबद्ध ग्राफ-सीरीज सिमेंटिक्स (graded graph-series semantics) प्रस्तुत करता है, जो यह प्रदर्शित करता है कि कैसे एबेल रेगुलराइजेशन (Abel regularization) और फ्रेडहोम डिटर्मिनेंट्स (Fredholm determinants) पुनरावर्ती परिभाषाओं को हल कर सकते हैं और फीडबैक लूप्स को इस तरह अभिलक्षणित कर सकते हैं कि जैसे-जैसे रेगुलराइजेशन पैरामीटर्स एकता की ओर बढ़ते हैं, मानक न्यूनतम-फिक्स्ड-पॉइंट (least-fixed-point) डिनोटेशन्स पुनः प्राप्त होते हैं।
यह शोध पत्र एल्टन (Elton) को प्रस्तुत करता है, जो एक उच्च-क्रम पृथक्करण तर्क (higher-order separation logic) है जिसमें अज्ञात प्रतिकूल कोड वाले संभाव्य प्रोग्रामों में त्रुटि सीमाओं और सुरक्षा गुणों को औपचारिक रूप से सत्यापित करने के लिए नवीन "अर्न संसाधनों" (urn resources) और विलंबित नमूनाकरण तंत्रों (delayed sampling mechanisms) का उपयोग किया गया है, जिसके सभी प्रमाण रॉक (Rocq) प्रूफ़ असिस्टेंट में मशीनीकृत किए गए हैं।