1105 पेपर
यह शोध पत्र प्लॉटकिन-शैली के बाइंडिंग हस्ताक्षरों (Plotkin-style binding signatures) द्वारा पैरामीटराइज्ड एगडा (Agda) के लिए एक जेनेरिक, सुव्यवस्थित स्थानीयतः नामहीन सिंटैक्स प्रतिनिधित्व (locally nameless syntax representation) प्रस्तुत करता है, जो अल्फा-रूपांतरण (alpha-conversion) के अधीन नैइव नेमफुल सिंटैक्स के विरुद्ध इसकी पर्याप्तता को सिद्ध करता है और उदाहरणों के माध्यम से इसकी उपयोगिता को प्रदर्शित करता है।
यह शोधपत्र सेट ऑटोमेटा (set automata) को पेश करके और यह सिद्ध करके कि यह तर्क (logic) ठीक तभी निर्णय योग्य (decidable) है जब अंतर्निहित मोनोइड (monoid) रैखिक रूप से क्रमबद्ध द्वि-पक्षीय आदर्शों (linearly ordered two-sided ideals) के साथ इडेम्पोटेंट (idempotent) हो, गार्डेड रेगुलर प्रेडिकेट्स (guarded regular predicates) के साथ विस्तारित डेटा वर्ड्स (data words) पर दो-चर तर्क (two-variable logic) की निर्णयक्षमता स्थापित करता है, जो इस समस्या को ऑर्डर्ड मल्टीकाउंटर ऑटोमेटा (ordered multicounter automata) की रिक्तता (emptiness) में अपचयित करके प्राप्त किया गया है।
यह शोधपत्र TreeWidzard को प्रस्तुत करता है, जो एक एकीकृत इंजन है जो जटिल ग्राफ गुणों को निर्धारित करने और स्वचालित प्रमेय प्रमाण (automated theorem proving) का समर्थन करने के लिए ट्रेewidth-आधारित डायनेमिक प्रोग्रामिंग एल्गोरिदम के विकास और संयोजन को सुगम बनाता है।
यह शोध पत्र मूव प्रोवर (Move Prover) के लिए एक स्पेसिफिकेशन इन्फरेंस टूल प्रस्तुत करता है जो वेरिफिकेशन स्पेसिफिकेशन्स को स्वचालित रूप से उत्पन्न करने और परिष्कृत करने के लिए साउंड वीकेस्ट-प्रीकंडीशन (weakest-precondition) विश्लेषण को एक एजेंटिक कोडिंग CLI के साथ समन्वित करता है, जो लूप इनवैरिएंट्स (loop invariants) और स्ट्रक्चरल इनवैरिएंट्स (structural invariants) जैसी जटिल प्रॉपर्टीज को संभालते हुए मैन्युअल बॉयलरप्लेट को प्रभावी ढंग से कम करता है।
यह शोध पत्र धनात्मक समांग फलन (positively homogeneous functionals) के रूप में सामान्य पूर्व अनुमानों (general previsions) की जांच करता है, यह प्रदर्शित करते हुए कि उन्हें उपरेखीय (sublinear) पूर्व अनुमानों के इन्फिमा (infima) और अतिरेखीय (superlinear) पूर्व अनुमानों के सुप्रा (suprema) के रूप में निरूपित किया जा सकता है, जिससे एक दोहरे पावर्सपेस निर्माण (double powerspace construction) के माध्यम से पूर्व अनुमानों के स्थानों और विशिष्ट हाइपरस्पेस के बीच होमियोमॉर्फिज्म (homeomorphisms) स्थापित होते हैं।
यह शोध पत्र मैसेज पासिंग न्यूरल नेटवर्क्स (MPNNs) की बहुपद गणना क्षमताओं (polynomial counting capabilities) की जांच करता है, जो यह प्रदर्शित करता है कि वे मीन एग्रीगेशन (mean aggregation) का उपयोग करके, विशेष रूप से रेगुलर ग्राफ, नॉन-नेस्टेड मोडैलिटीज या ट्री-लाइक संरचनाओं जैसी स्थितियों के तहत, नोड-लेबल वाले ग्राफ में वैश्विक और विशिष्ट स्थानीय बहुपद बाधाओं (global and specific local polynomial constraints) को सत्यापित कर सकते हैं।
यह शोध पत्र यह स्थापित करता है कि मॉड्युलो काउंटिंग के साथ प्रथम-क्रम तर्क (FOMOD), हान्फ़ सामान्य रूप (Hanf normal form) को अनुकूलित करके और एक नवीन संख्या-सिद्धांत संबंधी "पैचेबिलिटी" (patchability) स्थिति को प्रस्तुत करके, परिमित ग्राफों (सीमित डिग्री और घटक आकार) पर स्थिर समय में परीक्षण योग्य है, जिससे ऐसे वर्गों के लिए गणना के साथ मोनैडिक सेकंड-ऑर्डर तर्क की स्थिर-समय परीक्षण योग्यता के संबंध में एक खुले प्रश्न को हल किया गया है।
यह शोध पत्र विजातीय आंशिक प्रस्तावात्मक मॉडलों (disjoint partial propositional models) की गणना के लिए एक नवीन दृष्टिकोण प्रस्तावित करता है जो कॉन्फ्लिक्ट-ड्रिवन क्लॉज-लर्निंग, क्रोनोलॉजिकल बैकट्रैकिंग और इम्पलिकेंट श्रिंकिंग को एकीकृत करके ब्लॉकिंग क्लॉज की आवश्यकता को समाप्त करता है, जिससे पारंपरिक विधियों से जुड़ी मेमोरी और प्रदर्शन की सीमाओं को दूर किया जा सके।
यह शोध पत्र दो नवीन सॉल्वर, tabularAllSAT और tabularAllSMT पेश करता है, जो ब्लॉकिंग क्लॉज़ (blocking clauses) पर निर्भर हुए बिना SAT और SMT समस्याओं के लिए विलगित संतुष्ट असाइनमेंटों (disjoint satisfying assignments) को कुशलतापूर्वक सूचीबद्ध करने के लिए क्रोनोलॉजिकल बैकट्रैकिंग के साथ कॉन्फ्लिक्ट-ड्रिवन क्लॉज लर्निंग और एक आक्रामक इम्पलीकेंट श्रिंकिंग एल्गोरिदम का उपयोग करते हैं।
यह शोध पत्र प्रदर्शित करता है कि पदानुक्रमित (hierarchical) थ्योरम प्रूवर, शिक्षक ट्रेस (teacher traces) से पुन: प्रयोज्य प्रमाण संरचनाओं को सीखकर, फ्लैट प्रूवर्स की तुलना में सैंपल कॉम्प्लेक्सिटी (sample complexity) में घातीय कमी प्राप्त करते हैं, जिससे वे फ्लैटेड निरूपणों (flattened representations) में निहित कठिन उप-प्रमाणों की अनावश्यक पुनरावृत्ति से बच जाते हैं।