1115 पेपर
यह शोधपत्र औपचारिक गणित के लिए "मुक्त दृष्टिकोण" (free approach) का प्रस्ताव करता है, जो जटिल, प्रमाणन-केंद्रित मानक पद्धति का एक सुलभ विकल्प है और जो हर विवरण को यांत्रिक रूप से सत्यापित करने की बाध्यता को हटाकर औसत अभ्यासकर्ताओं के लिए संचार और उपयोगिता को प्राथमिकता देता है।
यह शोध पत्र प्रकट करता है कि ट्रांसफॉर्मर संपीड़न संवेदनशीलता विशिष्ट मैट्रिक्स प्रकारों में पांच आदेशों (orders of magnitude) तक भिन्न होती है, जो यह प्रदर्शित करता है कि जहाँ लियापुनोव स्थिरता (Lyapunov stability) त्रुटि संकुचन सुनिश्चित करती है, वहीं आर्किटेक्चर-विशिष्ट अतिरेक (architecture-specific redundancy) मजबूती के लिए समान रूप से महत्वपूर्ण है, एक ऐसा निष्कर्ष जिसे व्यापक अनुभवजन्य परीक्षणों के माध्यम से मान्य किया गया है और दस मशीन-जाँचा गया लीन 4 (Lean 4) प्रमेय द्वारा औपचारिक रूप से सत्यापित किया गया है।
यह शोधपत्र एक बहुपद-समय (polynomial-time) एल्गोरिदम प्रस्तुत करता है जो स्थानीय संक्रमणों (local transitions) पर एक एकदिष्ट ऑपरेटर (monotone operator) के उच्चतम स्थिर बिंदु (greatest fixed point) की गणना करके, स्व-अक्षम (self-disabling) प्रक्रियाओं के पैरामीटराइज्ड सममित एकदिशीय वलयों (parameterized symmetric unidirectional rings) में लाइवलॉक की उपस्थिति का निर्णय लेता है, जिससे स्पष्ट खोज (explicit search) के बिना सभी वलय आकारों के लिए लाइवलॉक स्वतंत्रता को प्रमाणित किया जाता है।
यह शोध पत्र "ट्री-कनेक्टेडनेस" (tree-connectedness) की परिष्कृत अवधारणा प्रस्तावित करके आर्बोरियल श्रेणियों (arboreal categories) में "पाथ्स आर कनेक्टेड" (paths are connected) अभिगृहीत की आलोचना करता है ताकि इसकी अपर्याप्तताओं को हल किया जा सके और आवश्यक गुणों को संरक्षित किया जा सके, और आगे यह स्थापित करता है कि पाथ फनक्टर (path functor) एक स्ट्रीट फाइब्रेशन (Street fibration) है।
यह शोध पत्र यह स्थापित करता है कि जबकि जनरेटिव सिस्टम (उत्पादक प्रणालियों) का विस्तार उनकी क्षमता को बढ़ा सकता है, वे कार्य कवरेज (टास्क कवरेज) में स्पर्शोन्मुखी घटते प्रतिफल (एसिम्प्टोटिक डिमिनिशिंग रिटर्न्स) और गोडेल-टार्स्की-लोब सिद्धांतों से प्राप्त तर्क संबंधी मौलिक सीमाओं का सामना करते हैं।
यह शोध पत्र को-ब्यूची ऑटोमेटा (co-Büchi automata) की श्रृंखलाओं (COCOA) की संक्षिप्तता का विश्लेषण करता है, यह प्रदर्शित करते हुए कि यद्यपि वे नियतात्मक पैरिटी ऑटोमेटा (deterministic parity automata) की तुलना में घातीय रूप से अधिक संक्षिप्त हो सकते हैं, लेकिन यह लाभ वियोजन (disjunction), संयोजन (conjunction), या पूरकता (complementation) जैसे बुलियन ऑपरेशनों को करने पर समाप्त हो जाता है, जिनके लिए आकार में घातीय वृद्धि आवश्यक होती है।
यह शोध पत्र एक नवीन, गतिशील रूप से पुन: प्रोग्राम करने योग्य रनटाइम मॉनिटर प्रस्तावित करता है जिसे सत्यापन के अधीन सिस्टम (system under verification) के समान ही डाई पर मानक सेल का उपयोग करके कार्यान्वित किया गया है, जो 0.55 mm² के संक्षिप्त फुटप्रिंट और 1.25 GHz की ऑपरेटिंग फ्रीक्वेंसी के साथ बाउंडेड-टाइम MTL गुणों की उच्च-गति, एट-स्पीड मॉनिटरिंग को सक्षम बनाता है।
यह शोध पत्र ट्यूरिंग डिग्रियों (Turing degrees) का आर्थर-निमूए-मर्लिन डिग्रियों (Arthur-Nimue-Merlin degrees) में एक क्रम-विपरीत एम्बेडिंग (order-reversing embedding) निर्मित करता है, जो "सह-ट्यूरिंग डिग्रियों" (co-Turing degrees) के एक नए वर्ग को परिभाषित करता है और इस सामान्यीकृत ढांचे के भीतर स्वाभाविक रूप से एम्बेडेड ट्यूरिंग डिग्रियों के साथ उनके क्रम-सिद्धांत संबंधी संबंध का विश्लेषण करता है।
यह शोध पत्र PRODSAT-QSAT प्रस्तुत करता है, जो एक CDCL-शैली का एल्गोरिदम है जो एक विभाजित ब्लॉक स्फीयर (Bloch sphere) की खोज करने और उत्पाद-अवस्था (product-state) की असंतोषजनकता को सिद्ध करने के लिए साउंड संघर्ष खंड (sound conflict clauses) उत्पन्न करने हेतु एक ज्यामितीय सिद्धांत सॉल्वर का उपयोग करके क्वांटम -SAT इंस्टेंस की संतुष्टि (satisfiability) का निर्धारण करता है।
यह शोधपत्र डिस्क्रिप्शन लॉजिक EL का एक नया सुलभ विस्तार प्रस्तावित करता है जो नकारात्मक बायोमेडिकल ज्ञान को दर्शाने के लिए निषेध (negation) के एक दुर्बल रूप को शामिल करता है, जिसे तार्किक कंस्ट्रक्टर्स के लिए श्रेणीगत अर्थविज्ञान (categorical semantics) को पेश करके और विशिष्ट गुणों को चुनिंदा रूप से हटाकर प्राप्त किया गया है जो जटिलता (intractability) के लिए उत्तरदायी हैं, जबकि मानक EL की तुलना में अधिक अभिव्यंजक क्षमता बनाए रखी गई है।