1117 पेपर
यह शोध पत्र एक समान प्रिमिटिव रिकर्सिव कंपाइलर का निर्माण करके प्राकृतिक संख्याओं पर एकल क्यूबिक डियोफैन्टीन समीकरणों की संतुष्टि (satisfiability) की -पूर्णता और अनिश्चितता (undecidability) को स्थापित करता है, जो अंकगणितीय प्रमाणयोग्यता को क्यूबिक बाधाओं में अनुवादित करता है, और अंततः रोक (Rocq) में मशीनीकरण के माध्यम से सत्यापित एक एकल स्पष्ट सार्वभौमिक क्यूबिक बहुपद प्रदान करता है।
यह शोध पत्र एक न्यूरो-सिम्बोलिक दृष्टिकोण प्रस्तावित करता है जो बड़े भाषा मॉडल (Large Language Models) को बाधा समाधानकर्ताओं (constraint solvers) के साथ सहक्रियात्मक रूप से एकीकृत करता है, ताकि सहायक लेम्मा (auxiliary lemmas) को पुनरावृत्ति के माध्यम से उत्पन्न और सत्यापित किया जा सके, जिससे अत्याधुनिक समाधानकर्ताओं की तुलना में इंडक्टिव डेफिनिशन (inductive definitions) से जुड़ी बाधाओं को हल करने की क्षमता में महत्वपूर्ण सुधार होता है।
यह शोध पत्र विवरण तर्क (description logic) अवधारणाओं में "मॉडल परिवर्तन" (model change) के लिए एक औपचारिक ढांचे को प्रस्तुत करता है, जो निष्कासन (eviction), प्राप्ति (reception) और संशोधन (revision) के बीच अंतर करता है, और यह प्रदर्शित करता है कि संशोधन एक विशिष्ट प्रक्रिया है जिसे अन्य दो के संयोजन में सरल रूप से कम नहीं किया जा सकता है, जबकि EL और ALC लॉजिक के भीतर उनकी अनुकूलता का विश्लेषण किया जाता है।
यह शोध पत्र स्पैन (spans) का उपयोग करके संभाव्य मॉडलों के बीच "व्याख्या" की एक श्रेणीगत धारणा प्रस्तुत करता है, जो यह प्रदर्शित करता है कि प्रत्येक स्थानीय रूप से-परिमित संभाव्य सिद्धांत एक फन्क्टरल निर्माण (functorial construction) के माध्यम से एक सुस्पष्ट, कैनोनिकल शास्त्रीय प्रतिनिधित्व स्वीकार करता है।
LTLGuard एक मॉड्यूलर फ्रेमवर्क है जो संसाधन-कुशल ओपन-वेट लैंग्वेज मॉडल्स (4B–14B पैरामीटर्स) को इटरेटिव कंसिस्टेंसी चेकिंग और रिफाइनमेंट के लिए लाइटवेट सिम्बॉलिक रीजनिंग के साथ कंस्ट्रेंड जनरेशन को जोड़कर, अनौपचारिक आवश्यकताओं से सही और संघर्ष-मुक्त लीनियर टेम्पोरल लॉजिक (LTL) स्पेसिफिकेशन जेनरेट करने में सक्षम बनाता है।
यह शोध पत्र यह प्रदर्शित करता है कि जबकि सीमित ट्यूरिंग मशीनें टेम्पोरल ओवरहेड के कारण स्व-प्रमाणन (self-certification) प्राप्त नहीं कर सकती हैं, परिमित हैल्टिंग अवलोकनों की पुनरावृत्ति प्रगति एक आरोही -श्रंखला (ascending -chain) बनाती है जिसका स्कॉट सीमा (Scott limit) न्यूनतम स्थिर बिंदु (least fixed point) प्रदान करती है, जो प्रभावी रूप से डायगोनलाइजेशन के निरंतर विलंबन के माध्यम से हैल्टिंग समस्या का समाधान करती है।
यह शोधपत्र प्रथम-क्रम तर्क (फर्स्ट-ऑर्डर लॉजिक) में कनेक्शन कैलकुली के लिए एक नवीन SAT-आधारित दृष्टिकोण प्रस्तुत करता है जो स्वयं प्रमाण खोज संरचना (प्रूफ सर्च स्ट्रक्चर) को एनकोड करता है, जिसमें सिमेट्री ब्रेकिंग के साथ तीन विशिष्ट एनकोडिंग प्रस्तुत की गई हैं और स्वचालित तर्क (ऑटोमेटेड रीजनिंग) को आगे बढ़ाने के लिए उन्हें नए सॉल्वर upCoP में कार्यान्वित किया गया है।
यह शोध पत्र एक-चर प्रथम-क्रम मोडल लॉजिक के स्वतंत्र संलयन (independent fusion) में क्रिपके पूर्णता (Kripke completeness) और निर्णयक्षमता (decidability) के संरक्षण की जांच करता है, जो यह प्रदर्शित करता है कि ये गुण विस्तारक (expanding) और स्थिर डोमेन (constant domain) दोनों अर्थों के तहत समानता (equality) के बिना बने रहते हैं, लेकिन जब समानता और गैर-कठोर स्थिरांक (non-rigid constants) पेश किए जाते हैं तो डायोफेंटाइन समीकरणों (Diophantine equations) के एन्कोडिंग के कारण विफल हो जाते हैं, और साथ ही यह भी स्थापित करता है कि परिमित मॉडल गुण (finite model property) केवल स्थानीय मामले (local case) में ही संरक्षित रहता है।
यह शोध पत्र क्रोनेकर उत्पाद और डायरेक्ट सम (direct sum) मोनोइडल संरचनाओं के अंतर्गत एक ग्राफ़िकल स्ट्रिंग डायग्राम फ्रेमवर्क के भीतर स्टोकेस्टिक मैट्रिक्स श्रेणियों के मात्रात्मक संवर्धन (quantitative enrichments) के रूप में अभिलक्षणित करके, कुलबैक-लीब्लर और रेनी डाइवर्जेंस के लिए पूर्ण आरेखीय स्वयंसिद्धीकरण (diagrammatic axiomatisations) प्रस्तुत करता है।
यह शोध पत्र शास्त्रीय प्रथम-क्रम संबंध कलन (first-order connection calculus) के लिए एक बाधा शिक्षण (constraint learning) दृष्टिकोण प्रस्तुत करता है और उसे पुनरावृत्ति से परिष्कृत करता है, जो पूर्णता को बनाए रखते हुए गैर-अभिसारी प्रमाण खोज (non-confluent proof search) में बैकट्रैकिंग को महत्वपूर्ण रूप से कम करता है।