1086 पेपर
यह शोध पत्र "सूचना नाभिक" (information nuclei) के माध्यम से कैप्चर किए गए एफ़ाइन सूचना प्रसार (affine information propagation) को संकुचन (contraction) से अलग करके, कार्यात्मक व्याख्याओं (functional interpretations) के लिए एक एकीकृत ढांचे को प्रस्तुत करता है, जिससे निरंतरता (continuity) जैसी सहायक जानकारी के साथ निकाले गए रियलाइजर्स (realizers) के व्यवस्थित विनिर्देशन और संवर्धन को सक्षम बनाया जा सके।
यह शोध पत्र एक न्यूरो-सिम्बोलिक एआई (Neuro-Symbolic AI) ढांचे का प्रस्ताव करता है जो शुद्ध रूप से न्यूरल कानूनी प्रणालियों में निहित मतिभ्रम (hallucination) के जोखिमों को कम करने के लिए कोरियाई यातायात अपराधों हेतु सजा के पूर्वानुमान और दस्तावेज़ प्रारूपण की सटीकता और विश्वसनीयता बढ़ाने के लिए अर्थपूर्ण निष्कर्षण (semantic extraction) हेतु लार्ज लैंग्वेज मॉडल्स (Large Language Models) को नियतात्मक वैधानिक गणनाओं (deterministic statutory calculations) के लिए सेटिस्फिएबिलिटी मॉडलो थ्योरीज (Satisfiability Modulo Theories) सॉल्वर्स के साथ जोड़ता है।
यह शोध पत्र एक्शन और पब्लिक अनाउंसमेंट लॉजिक्स (AMLFI1 और PALFI1) को परिभाषित करके पैराकंसिस्टेंसी के लिए एक गतिशील ढांचे को प्रस्तुत करता है जो मौजूदा एपिस्टेमिक पैराकंसिस्टेंट सिस्टम्स का विस्तार करते हैं, जिससे अनंतिम विरोधाभासों को प्राप्त करने और उन्हें हल करने को औपचारिक रूप देना सक्षम होता है, साथ ही उनकी साउंडनेस और कम्प्लीटनेस को सिद्ध करना भी संभव होता है।
यह शोध पत्र रेडियो -लेबलिंग समस्या के लिए एक सटीक, वृद्धिशील (incremental) SAT-आधारित ढांचे को प्रस्तुत करता है जो 38 उदाहरणों के लिए नए सर्वश्रेष्ठ-ज्ञात समाधान स्थापित करके और 146 बेंचमार्क ग्राफों में से 109 के लिए इष्टतमता (optimality) को प्रमाणित करके अत्याधुनिक वाणिज्यिक सॉल्वरों और ह्यूरिस्टिक्स से बेहतर प्रदर्शन करता है।
यह शोध पत्र लीनियर -कैलकुलस के मॉडलों पर तीन बीजगणितीय दृष्टिकोणों—लीनियर -टर्म्स के ऑपेरैड (operad), करी के -बीजगणितों (Curry's -algebras) के एक लीनियर एनालॉग, और सेमीक्लोज्ड ऑपेरैड्स (semiclosed operads)—के बीच तुल्यता स्थापित करता है, साथ ही बाद वाले के लिए एक परिमित समीकरण प्रस्तुति (finite equational presentation) प्रदान करता है और प्रेशेफ श्रेणियों (presheaf categories) में रिफ्लेक्सिव ऑब्जेक्ट्स (reflexive objects) के माध्यम से स्कॉट के रिप्रेजेंटेशन थ्योरम का एक लीनियर एनालॉग सिद्ध करता है।
यह शोधपत्र क्वांटम टर्म रीराइट सिस्टम्स (QTRS) को शास्त्रीय टर्म रीराइट सिस्टम्स के एक भौतिक रूप से साकार विस्तार के रूप में प्रस्तुत करता है जो जटिलता विश्लेषण को सक्षम बनाता है और टर्मिनेटिंग QTRS तथा क्वांटम सर्किट के यूनिफॉर्म परिवारों के बीच एक पत्राचार स्थापित करके क्वांटम पॉलिनॉमियल टाइम () में गणनीय फलनों के वर्ग को अभिलक्षित करता है।
यह शोध पत्र गैर-निश्चयात्मक मैट्रिसेस (nondeterministic matrices) के ढांचे के भीतर एक नए त्रि-मूल्यवान सममित गैर-निश्चयात्मक विच्छेदन (three-valued symmetric nondeterministic disjunction) का प्रस्ताव करता है ताकि रिएक्टिव सिस्टम में कम्प्यूटेशनल त्रुटियों का एक तार्किक औपचारिकीकरण प्रदान किया जा सके जो क्रमबद्ध मूल्यांकन विषमताओं को समाप्त करते हुए क्रमविनिमेयता (commutativity) और परिचालन समरूपता (operational symmetry) को संरक्षित करता है।
यह शोध पत्र स्पष्ट प्रतिस्थापनों (explicit substitutions) वाले एक कैलकुलस के लिए एक नए टर्म एक्सपेंशन को प्रस्तुत करता है ताकि स्पष्ट प्रतिस्थापनों वाले लैम्ब्डा-टर्म्स और बौडोल के रिसोर्स-अवेयर लैम्ब्डा-कैलकुलस विद मल्टीप्लिसिटीज के बीच एक पत्राचार स्थापित किया जा सके, जो सबस्ट्रक्चरल टाइप सिस्टम्स में टर्म एक्सपेंशन के पिछले अनुप्रयोगों का विस्तार करता है।
यह शोधपत्र एक नए डायनेमिक लॉजिक के लिए एक पूर्ण स्वयंसिद्धीकरण (axiomatization) और एक टर्मिनेटिंग, साउंड और कंप्लीट टॅब्लो कैलकुलस प्रस्तुत करता है, जिसे विशेष रूप से डोलेव-याओ घुसपैठिया मॉडल (Dolev-Yao intruder model) को एकीकृत करके प्रतिकूल वातावरण में क्रिप्टोग्राफिक प्रोटोकॉल की प्रमाणिकता और सुरक्षा को सत्यापित करने के लिए डिज़ाइन किया गया है।
यह शोध पत्र डे ब्रुइजन नोटेशन (de Bruijn notation) में लीनियर लैम्ब्डा-कैलकुलस के लिए एक टाइपिंग सिस्टम प्रस्तुत करता है जो होडास और मिलर के रिसोर्स कंजम्पशन मॉडल का उपयोग करके बिना ऑक्युरेंस चेक (occurrence checks) के लिनियरिटी की गारंटी देता है, और तत्पश्चात इसके सब्जेक्ट रिडक्शन (subject reduction) गुण को सिद्ध करता है।