1105 पेपर
यह शोध पत्र एक एकीकृत टेम्पोरल डैटलॉग (Temporal Datalog) ढांचे में उन्हें मैप करके विजातीय इवेंट स्पेसिफिकेशन भाषाओं की तुलना करने की चुनौती को संबोधित करता है और उच्च-वेग वाले डेटा स्ट्रीम पर कुशल, सामान्यीकरण योग्य कंपोजिट इवेंट रिकग्निशन को सक्षम करने के लिए स्ट्रीमिंग ट्रिगर ग्राफ्स (Streaming Trigger Graphs) पेश करता है।
यह शोध पत्र SHACL दस्तावेज़ समावेशन (document containment) की निर्णयक्षमता (decidability) की जांच करता है, जो यह सिद्ध करता है कि यह समस्या समर्थित और स्थिर मॉडल सिमेंटिक्स (supported and stable model semantics) के तहत अनिर्णायक (undecidable) है, लेकिन हाइब्रिड म्यू-कैलकुलस (hybrid mu-calculus) में एक नवीन अनुवाद के माध्यम से वेल-फाउंडेड सिमेंटिक्स (well-founded semantics) के तहत सिंगल एक्सपोनेंशियल समय में निर्णयक्षम है।
यह शोध पत्र 'एल्जेब्रा ऑफ इटरेटिव कंस्ट्रक्शन्स' (AIC) को प्रस्तुत करता है, जो पूर्ण लैट्टिस (complete lattices) पर फिक्स्ड पॉइंट इटरेशन के बारे में तर्क करने के लिए एक विशुद्ध बीजगणितीय ढांचा है, जो स्वचालित प्रमेय सिद्ध करने में सक्षम बनाता है, टार्स्की-कानटोरविच सिद्धांत जैसे मौजूदा परिणामों का सामान्यीकरण करता है, और इसके अपने स्वयंसिद्धों (axiomatization) की सैद्धांतिक सीमाओं को स्थापित करता है।
यह शोध पत्र iSMC प्रस्तुत करता है, जो कि जस्टिस आवश्यकताओं (justice requirements) के साथ कंप्यूटेशन ट्री लॉजिक (CTL) के लिए पहला स्व-प्रमाणित (self-certifying), BDD-आधारित सिम्बोलिक मॉडल चेकर है, जो QBF-सॉल्विंग तकनीक से अनुकूलित एक संवादात्मक प्रमाणन प्रक्रिया के माध्यम से अपने उत्तरों की शुद्धता की गारंटी देता है।
यह शोध पत्र ट्री ट्रांसडक्शन (tree transductions) के एक नए वर्ग को प्रस्तुत और अभिलक्षित करता है, जिसे रैखिक आकार-से-ऊंचाई वृद्धि वाले ट्री-वॉकिंग हेनी मशीनों (tree-walking Hennie machines) द्वारा परिभाषित किया गया है, जो नियमित ट्री फलनों (regular tree functions) का सख्ती से विस्तार करता है और यह दिखाया गया है कि यह विशिष्ट संयोजनों के अंतर्गत बंद है और योगात्मक टुपल्स (additive tuples) वाले एक रैखिक लैम्ब्डा-कैलकुलस (linear lambda-calculus) के समकक्ष है।
यह शोधपत्र एक हाइब्रिड SAT-सॉल्विंग फ्रेमवर्क प्रस्तावित करता है जो उच्च-सहमति मान्यताओं (high-agreement assumptions) के साथ कॉन्फ्लिक्ट-ड्रिवन क्लॉज लर्निंग (CDCL) को निर्देशित करने के लिए प्रोबेबिलिस्टिक-बिट आइसिंग सैम्पलर्स का लाभ उठाता है, जिससे विशिष्ट 3-SAT बेंचमार्क पर खोज प्रयास में महत्वपूर्ण कमी आती है और साथ ही यह निर्धारित करने के लिए मशीन लर्निंग गेट्स का उपयोग करता है कि ऐसा मार्गदर्शन कब फायदेमंद होता है।
यह शोध पत्र तर्क के लिए एक निर्णय प्रक्रिया प्रस्तुत करता है, जो अनबाउंडेड (unbounded) चरों की अनुमति देने वाले परिमित पूर्णांक अंतरालों के साथ परिमित सेट थ्योरी का विस्तार करता है, और एक एलीवेटर एल्गोरिदम के लिए इनवेरिएंस लेम्मा (invariance lemmas) को स्वचालित रूप से सत्यापित करने के लिए टूल के माध्यम से इसकी व्यावहारिक उपयोगिता को प्रदर्शित करता है।
यह योगदान अट्रैक्टर एफसीएम (Attractor FCM) प्रस्तुत करता है, जो एक नवीन, ग्रेडिएंट-डिसेन्ट-आधारित और भौतिक रूप से बाधित फजी कॉग्निटिव मैप है, जो अवशेष स्मृति (residual memory), बैकप्रोपैगेशन थ्रू टाइम और एक फिक्स्ड-पॉइंट एंकर का लाभ उठाता है ताकि एक नया लर्निंग एल्गोरिदम सक्षम किया जा सके जो कुशल, कॉज़ली मास्क की गई त्रुटि न्यूनीकरण के लिए न्यूटन विधि को एडेप्टिव ग्रेडिएंट डिसेन्ट के साथ जोड़ता है।
यह शोध पत्र यह प्रदर्शित करता है कि सभी सुदृढ़ (robust) उदाहरणों के लिए सुदृढ़ आंशिक एल्गोरिदम के माध्यम से वास्तविक रैखिक और अफ़ाइन लूप्स का सार्वभौमिक समापन प्रभावी रूप से निर्णायक (decidable) है, क्योंकि गैर-सुदृढ़ मामलों का समुच्चय एक लेबेग माप शून्य (Lebesgue measure zero) का गठन करता है।
यह शोध पत्र वास्तविक डिफरेंशियल-फॉर्म पुलबैक (differential-form pullbacks) का उपयोग करते हुए स्मूथ सिंगुलर क्यूब्स के लिए स्टोक्स प्रमेय का एक व्यापक, त्रुटिहीन (sorry-free) Lean 4 औपचारिक रूप (formalization) प्रस्तुत करता है, साथ ही mathlib4 के साथ सेतु स्थापित करता है, जैसी चेन-लेवल (chain-level) गुणों को सत्यापित करता है, और हैरिसन के HOL Light औपचारिक रूप के साथ कार्यान्वयन की तुलना करता है।