1115 पेपर
यह शोधपत्र सिंथेटिक टैट कंप्यूटेबिलिटी (synthetic Tait computability) को मोडैलिटीज़ को संभालने के लिए विस्तारित करके मल्टीमॉडल टाइप थ्योरी (Multimodal Type Theory - MTT) के नॉर्मलाइजेशन को स्थापित करता है, जिससे गार्डेड रिकर्सन (guarded recursion) और इंटरनलाइज्ड पैरामीट्रिसिटी (internalized parametricity) जैसे विभिन्न मोडल सिस्टम के लिए एक एकीकृत टाइप-चेकिंग एल्गोरिदम प्राप्त होता है।
यह शोध पत्र उन टर्मिनेटिंग टैबलो कैलकुली (terminating tableau calculi) को प्रस्तुत करता है जो कड़ाई से आंशिक रूप से क्रमबद्ध (strictly partially ordered), असीमित कड़ाई से आंशिक रूप से क्रमबद्ध (unbounded strictly partially ordered), और आंशिक रूप से क्रमबद्ध (partially ordered) एक्सेसिबिलिटी संबंधों वाले मॉडलों पर लागू होने पर हाइब्रिड लॉजिक के लिए पूर्ण (complete) हैं।
यह शोध पत्र अनंत अचक्रीय ग्राफ़ (infinite acyclic graphs) का उपयोग करके लायर्स पैराडॉक्स (liar paradox) की याब्लो की कोडिंग के संबंध में लेखक के पिछले विश्लेषण का अधिक व्यवस्थित निरंतरता प्रदान करता है।
यह शोध पत्र IPL-V के लिए एक नया कॉमन लिसप (Common Lisp) इंटरप्रेटर बनाकर और स्टेफरुड के 1963 के सोर्स कोड से 1956 के एआई (AI) प्रोग्राम को सफलतापूर्वक पुनर्जीवित करके, आधे दशक से अधिक समय में मूल लॉजिक थियोरिस्ट (Logic Theorist) के पहले सफल निष्पादन को प्रस्तुत करता है, जिसने *प्रिंसिपिया मैथमैटिका* (Principia Mathematica) के 23 में से 16 प्रमेयों को सफलतापूर्वक सिद्ध किया।
यह शोध पत्र पावर टर्म बहुपद बीजगणित (power term polynomial algebra) को प्रस्तुत करता है, जो एक नवीन मध्यवर्ती निरूपण है जो सहायक चरों के बिना संरचित मोनॉमियल्स और क्लॉज़ों को संक्षिप्त रूप से कूटबद्ध करके कंजंक्टिव नॉर्मल फॉर्म (CNF) और अल्जेब्रिक नॉर्मल फॉर्म (ANF) के बीच सेतु बनाता है, जिससे घातीय विस्फोट (exponential blowup) से बचते हुए कुशल प्रतीकात्मक हेरफेर और हाइब्रिड तर्क सक्षम होता है।
यह शोध पत्र \textit{s2n-bignum-bench} को प्रस्तुत करता है, जो कि प्रतिस्पर्धात्मक गणित में सफलता और वास्तविक दुनिया के औपचारिक सत्यापन (formal verification) के बीच के अंतर को संबोधित करने के लिए, HOL Light में औद्योगिक निम्न-स्तरीय क्रिप्टोग्राफिक असेंबली रूटीन के लिए मशीन-जांच योग्य प्रमाण उत्पन्न करने की लार्ज लैंग्वेज मॉडल्स (LLMs) की क्षमता का मूल्यांकन करने के लिए डिज़ाइन किया गया पहला सार्वजनिक बेंचमार्क है।
यह शोध पत्र लीन 4 (Lean 4) प्रूफ़ असिस्टेंट और मैथलिब (Mathlib) का उपयोग करते हुए समतल में शास्त्रीय समक्षेत्रीय असमानता (isoperimetric inequality) का एक औपचारिक सत्यापन प्रस्तुत करता है, जो एडोल्फ हर्ट्ज़ के विश्लेषणात्मक दृष्टिकोण का अनुसरण करता है ताकि यह सिद्ध किया जा सके कि दिए गए परिधि वाले सभी सरल बंद वक्रों में, वृत्त अद्वितीय रूप से घेरे गए क्षेत्र को अधिकतम करता है।
यह शोध पत्र पियर्स और ओसोरियो के मौलिक दृष्टिकोणों को टेम्पोरल (सामयिक) परिवेश में उन्नत करके, टेम्पोरल इंट्यूशनिस्टिक लॉजिक और टेम्पोरल लॉजिक प्रोग्रामिंग के बीच एक औपचारिक पत्राचार स्थापित करता है, जिससे टेम्पोरल इक्विलिब्रियम लॉजिक के माध्यम से टेम्पोरल आंसर सेट प्रोग्रामिंग की सैद्धांतिक नींव को गहरा किया जा सके।
यह शोध पत्र प्रथम-क्रम तर्क सूत्रों (first-order logic formulas) के सापेक्ष संबंधात्मक बीजगणक (relational algebra) की पूर्णता का एक वैकल्पिक बीजगणितीय प्रमाण प्रस्तुत करता है, जो एक नए रूपांतरण एल्गोरिदम को व्युत्पन्न करने के लिए सिलिंड्रिक बीजगणक (cylindric algebra) में इसके एम्बेडिंग (embedding) का लाभ उठाता है और अपूर्ण या अस्पष्ट सूचना को संभालने वाले मॉडलों तक इन परिणामों को विस्तारित करने के लिए आधार तैयार करता है।
यह शोध पत्र सेमिटोपोलॉजी पर आधारित थ्री-वैल्यूड मोडल लॉजिक के भीतर डिक्लेरेटिव एक्सियोमैटिक थ्योरीज़ के रूप में डिस्ट्रिब्यूटेड एल्गोरिदम को औपचारिक रूप से निर्दिष्ट करने के लिए एक नवीन फ्रेमवर्क प्रस्तावित करता है, जो वोटिंग, ब्रॉडकास्ट और एग्रीमेंट प्रोटोकॉल के लिए लीन 4 (Lean 4) में औपचारिक प्रमाणों द्वारा प्रदर्शित किया गया है, और एक सटीक, उच्च-स्तरीय एब्स्ट्रैक्शन प्रदान करता है जो आवश्यक सिस्टम गुणों को कैप्चर करने के साथ-साथ कठोर मानव और मशीन सत्यापन को सक्षम बनाता है।