1086 पेपर
यह शोधपत्र यह स्थापित करता है कि अनंत पिजनहोल सिद्धांतों (infinite pigeonhole principles) का पदानुक्रम, जब अंकगणितीय पदानुक्रम (arithmetic hierarchy) के विभिन्न स्तरों तक सीमित होता है, एक पुनरावृत्त जंप नियंत्रण निर्माण (iterated jump control construction) का उपयोग करके और कंप्यूटेबिलिटी-थ्योरेटिक एवं रिवर्स मैथमैटिकल परिप्रेक्ष्यों से इसके प्रथम-क्रम परिणामों का विश्लेषण करके पर सख्त है।
यह शोध पत्र लॉजिक-आधारित कंडीशनल क्रिटिकल पेयर्स (Logic-based Conditional Critical Pairs), पैरामीट्रिक कंडीशनल वेरिएबल पेयर्स (parametric Conditional Variable Pairs) और डाउन कंडीशनल पेयर्स (Down Conditional Pairs) नामक तीन विशिष्ट प्रकार के कंडीशनल पेयर्स को पेश करके, एक इक्विवेलेंस रिलेशन (equivalence relation) के मॉड्यूलो रीराइटिंग में कन्फ्लुएंस (confluence) सिद्ध करने के फ्रेमवर्क को कंडीशनल सिस्टम्स तक विस्तारित करता है, ताकि Maude जैसे सिस्टम्स में E-कन्फ्लुएंस (E-confluence) को सत्यापित या खंडित करने के लिए परिमित मानदंड स्थापित किए जा सकें।
यह शोधपत्र यह प्रदर्शित करता है कि सभी नियमित भाषाएँ (regular languages) प्रथम-क्रम तर्क (first-order logic) FC में परिभाषित नहीं होती हैं और बीजगणितीय, ऑटोमेटा-सैद्धांतिक, और संक्षिप्त नियमित अभिव्यक्ति मानदंडों का उपयोग करते हुए FC-परिभाषित नियमित भाषाओं का एक निर्णय योग्य (decidable) लक्षण वर्णन प्रदान करता है।
CircuitProver एक एजेंटिक Lean 4 फ्रेमवर्क है जो पैरामीटराइज्ड डिज़ाइनों और विनिर्देशों को निष्पादन योग्य मॉडलों में अनुवादित करके, मशीन-चेक्ड प्रमाणों का पुनरावृत्ति से निर्माण करके, और इन परिणामों को एक पुन: प्रयोज्य लाइब्रेरी में संकलित करके हार्डवेयर सत्यापन को स्वचालित करता है, जो वैनिला एजेंटों की तुलना में प्रमाण दक्षता और सफलता दर में महत्वपूर्ण सुधार करता है।
यह शोध पत्र लीन (Lean) थ्योरम प्रूवर में पाठ्यपुस्तक "मेज़र-थ्योरेटिक प्रोबेबिलिटी" (Measure-Theoretic Probability) को औपचारिक रूप से सत्यापित करने के एक चल रहे प्रोजेक्ट की रिपोर्ट करता है, जिसका लक्ष्य एक मशीन-चेक्ड साथी बनाना है जो गणितीय सत्यापन को बढ़ाने, धारणाओं को स्पष्ट करने और विश्वसनीय एआई-सहायता प्राप्त गणित का समर्थन करने के लिए पाठ्यपुस्तक के कथनों को मैथलिब (Mathlib) लाइब्रेरी के साथ जोड़ता है।
यह शोध पत्र यह प्रदर्शित करता है कि एक्सटेंशन प्रकार (extension types), जो पाथ प्रकार (path types) और नियंत्रित-अनफोल्डिंग तंत्र (controlled-unfolding mechanisms) जैसी विभिन्न अवधारणाओं को एकीकृत करते हैं, उन्हें बिना किसी नए अभिगृहीत या मॉडल के दो-स्तरीय प्रकार सिद्धांत (two-level type theory) के भीतर परिभाषित किया जा सकता है, जिससे उनके नियमों को प्रमेय के रूप में मान्य किया जा सकता है, यूनिवैलेंस (univalence) पर क्यूबिकल ग्लूइंग (cubical gluing) की संरक्षणीयता को सिद्ध किया जा सकता है, और इस खुले प्रश्न को हल करने का मार्ग प्रशस्त किया जा सकता है कि क्या क्यूबिकल प्रकार सिद्धांत (cubical type theories) बुक होटी (book HoTT) पर संरक्षणीय हैं।
यह शोध पत्र सकारात्मक और नकारात्मक नोड उदाहरणों से रिकर्सिव (recursive) SHACL शेप्स को डिस्क्रिप्शन लॉजिक ELI फ्रैगमेंट में सीखने की समस्या की जांच करता है, जो अस्तित्व (existence) और सबसे विशिष्ट फिटिंग (most specific fitting) गणना के लिए सटीक एक्सपोनेंशियल-टाइम ऊपरी सीमाएं स्थापित करता है और विशेष मामलों के लिए पॉलीनोमियल-टाइम समाधानों की पहचान करता है।
यह शोध पत्र "चयनात्मक विश्वसनीयता-सीमित विश्वास अद्यतन" (selective credibility-limited belief update) को प्रस्तुत करता है, जो एक नवीन ढांचा है जो मानक विश्वास अद्यतन मॉडलों को एपिस्टेमिक इनपुट्स को कमजोर, स्रोत-निर्भर प्रॉक्सी में बदलकर उन्नत करता है ताकि मिश्रित सूचना के केवल विश्वसनीय भागों को चयनात्मक रूप से स्वीकार किया जा सके, जिससे मौजूदा विश्वसनीयता-सीमित और कटात्सुनो-मेंडेलज़ोन दृष्टिकोणों को एकीकृत और कड़ाई से सामान्यीकृत किया जा सके।
यह शोध पत्र एक उच्च-प्रदर्शन, प्रमाण-उत्पादक (proof-producing) SAT फ्रेमवर्क प्रस्तुत करता है जो ज्यामितीय रूप से सूचित एन्कोडिंग, समरूपता भंग (symmetry breaking), और स्वतंत्र रूप से सत्यापन योग्य शुद्धता सुनिश्चित करने के लिए एक एकीकृत सत्यापन पाइपलाइन का लाभ उठाकर पूर्व में खुले क्वीन डोमिनेशन केस को हल करता है और के लिए गणना (enumeration) को सुधारता है।
यह शोध पत्र प्रदर्शित करता है कि इंटेंशनल टाइप थ्योरी (सेफ एगडा में औपचारिक रूप से प्रस्तुत) के भीतर प्रदर्शित सेटोइड्स, यूनिवर्स के साथ एक्सटेंशनल टाइप थ्योरी के लिए एक सिमेंटिक्स प्रदान कर सकते हैं, जिससे एक कोरोलरी के रूप में बाद की निरंतरता स्थापित होती है।