1115 पेपर
यह शोध पत्र लीन थ्योरम प्रूवर (Lean Theorem Prover) में ब्रुअत-टिट्स ट्री (Bruhat-Tits tree) के औपचारिककरण को प्रस्तुत करता है और ट्री पर हार्मोनिक कोचेन्स (harmonic cochains) से संबंधित एक परिणाम को सत्यापित करके इसकी उपयोगिता को प्रदर्शित करता है।
यह शोध पत्र TREBL को प्रस्तुत करता है, जो Event-B के लिए एक सापेक्ष पूर्ण टेम्पोरल लॉजिक (relative complete temporal logic) है जो स्टेट ट्रेसेस (state traces) पर लाइवनेस प्रॉपर्टीज (liveness properties) को व्यक्त करता है, इसके लिए सुदृढ़ व्युत्पन्न नियम (sound derivation rules) परिभाषित करता है, और यह सिद्ध करता है कि पर्याप्त परिष्कृत मशीनों (refined machines) में, जहाँ विशिष्ट वेरिएंट टर्म्स (variant terms) परिभाषित करने योग्य हों, वैध निहितार्थ (valid entailments) को हमेशा व्युत्पन्न किया जा सकता है।
यह शोध पत्र "टूल-इंड्यूस्ड मायोपिया" (TIM) की पहचान और लक्षण वर्णन करता है, जो एक ऐसी घटना है जहाँ टूल-ऑगमेंटेड लैंग्वेज मॉडल्स (TaLMs) गणितीय समस्याओं पर उच्च अंतिम-उत्तर सटीकता प्राप्त करते हैं लेकिन टूल आउटपुट को तर्क के विकल्प के रूप में उपयोग करने के कारण तर्कसंगत सुसंगतता में गिरावट का सामना करते हैं, और एक प्राथमिकता-अनुकूलन ढांचे का प्रस्ताव करता है ताकि मॉडल्स को टूल्स को तर्क के शॉर्टकट के बजाय सहायक साक्ष्य के रूप में उपयोग करने के लिए पुनर्गठित किया जा सके।
यह शोध पत्र क्लीनी-कार्टेशियन रिग श्रेणियों (Kleene-Cartesian rig categories) और उनके संबद्ध टेप आरेख (tape diagrams) को एक ऐसी ग्राफ़िकल नोटेशन के रूप में प्रस्तुत करता है जो आदेशात्मक प्रोग्रामों (imperative programs) और विभिन्न प्रोग्राम लॉजिकों को सुविधाजनक रूप से प्रदर्शित करने में सक्षम है।
यह शोध पत्र "कंपाइल टू कंप्रेस" (Compile to Compress) पेश करता है, जो एक लर्निंग-टू-रिफाइन फ्रेमवर्क है जो कुशल, वेरीफायर-गाइडेड ट्री सर्च को सक्षम करने के लिए कंपाइलर-जनरेटेड फेलियर मोड्स के संक्षिप्त सेट का लाभ उठाता है, जिससे मौजूदा लार्ज लैंग्वेज मॉडल प्रूवर्स की तुलना में काफी कम टेस्ट-टाइम कंप्यूट के साथ पुटनम बेंच (PutnamBench) पर अत्याधुनिक प्रदर्शन प्राप्त होता है।
यह शोध पत्र नियंत्रित निरंतरता के तर्क (L) के पदानुक्रम को प्रस्तुत करता है, जो औपचारिक विसंगति के तर्कों (Logics of Formal Inconsistency) का एक द्वि-आयामी वर्गीकरण है जो संदेहवाद से लेकर कट्टरपंथ तक विभिन्न स्तरों की विरोधाभासपूर्ण प्रतिबद्धता को मॉडल करता है, और इस परिवार तथा इसके विशिष्ट विस्तारों के लिए स्वैप संरचनाओं (swap structures), ट्विस्ट संरचनाओं (twist structures) और RN-मैट्रिसेस (RNmatrices) का उपयोग करते हुए सुदृढ़ और पूर्ण अर्थ संबंधी विवरण प्रदान करता है।
यह शोध पत्र प्लॉसिबल लॉजिक (PL) को प्रस्तुत करता है, जो कि डिफ़ेज़िबल रीजनिंग (defeasible reasoning) के लिए डिज़ाइन किया गया एक प्रथम-क्रम का गैर-संभाव्यता तर्क है, जो 17 प्रस्तावित सिद्धांतों का पालन करता है और तथ्यों एवं डिफ़ेज़िबल कथनों से तर्कसंगत निष्कर्ष निकालने के लिए आठ विशिष्ट तर्क एल्गोरिदमों का उपयोग करता है।
यह शोध पत्र प्रस्तावित -CCWL आइसोमोर्फिज्म टेस्ट, नव-परिचिय टोपोलॉजिकल काउंटिंग लॉजिक (TC), और एक टोपोलॉजिकल पेबल गेम के बीच सटीक समानता को सिद्ध करके टोपोलॉजिकल न्यूरल नेटवर्क के लिए एक तार्किक अभिव्यक्तता सिद्धांत स्थापित करता है, जिससे उन बाइनरी क्लासिफायर्स का सटीक वर्ग निर्धारित होता जिन्हें ये नेटवर्क प्रदर्शित कर सकते हैं।
यह शोध पत्र लार्ज लैंग्वेज मॉडल्स का उपयोग करके कैंडिडेट स्ट्रीमलाइनर कंस्ट्रेंट्स (candidate streamliner constraints) को जेनरेट और फ़िल्टर करने के माध्यम से StreamLLM दृष्टिकोण को आंसर सेट प्रोग्रामिंग (Answer Set Programming) के अनुकूल बनाता है, जिसके परिणामस्वरूप एक वर्चुअल बेस्ट एनकोडिंग प्राप्त होती है जो वास्तविक समस्या संरचनाओं को कैप्चर करके तीन ASP बेंचमार्क पर 4-5 गुना तक की गति वृद्धि (speedups) प्राप्त करती है।
यह शोध पत्र SCFO(ID) को प्रस्तुत करता है, जो एक नया सीक्वेंट कैलकुलस (sequent calculus) है जो स्थिर अर्थशास्त्र (stable semantics) के सिद्धांतों को अनुकूलित करके पिछले वाक्यात्मक (syntactic) सीमाओं को दूर करने के लिए, FO(ID) में सामान्य गैर-एकदिष्ट (non-monotone) आगमनात्मक परिभाषाओं (inductive definitions) के औपचारिक प्रमाणों का समर्थन करने हेतु मौजूदा LKID प्रणाली का विस्तार करता है।