1115 पेपर
यह शोधपत्र 'फॉर्मूला ऑफ द यूनिवर्सल लॉ लॉजिक' (FULL) प्रस्तुत करता है, जो एक मल्टी-सॉर्टेड क्वांटिफाइड मोडल लॉजिक है जो कांट के कैटेगोरिकल इम्पेरेटिव को औपचारिक रूप देता है ताकि आर्टिफिशियल मोरल एजेंट्स को पूर्व-कोडित नैतिक अंतर्ज्ञान पर निर्भर किए बिना उनके उद्देश्यों और पृष्ठभूमि ज्ञान के आधार पर कार्यों का मूल्यांकन करने में सक्षम बनाया जा सके।
यह शोध पत्र एक वृद्धिशील सुरक्षा प्रमाण ढांचे (incremental safety proof framework) को प्रस्तुत करता है जो जटिल प्रेरणिक अपरिवर्तनीयता (inductive invariants) को सरल घटकों में विघटित करने के लिए फॉरवर्ड रीजनिंग, टाइम-रिवर्स सिस्टम पर बैकवर्ड रीजनिंग और प्रोफेसी स्टेप्स को संयोजित करता है, जिससे सत्यापन के लिए खोज स्थान (search space) कम हो जाता है और Paxos और Raft जैसे वितरित सर्वसम्मति प्रोटोकॉल (distributed consensus protocols) पर इसकी प्रभावशीलता प्रदर्शित होती है।
यह शोध पत्र रजिस्टर सेट ऑटोमेटा (RSAs) का प्रस्ताव करता है, जो एक नवीन ऑटोमेटन मॉडल है जो बैकरेफरेंस (backreferences) वाले रेगुलर एक्सप्रेशंस के कुशल, नियत (deterministic) और सुदृढ़ मिलान को सक्षम करने के लिए सेट-आधारित ऑपरेशंस के साथ रजिस्टर ऑटोमेटा का विस्तार करता है, और साथ ही उनकी सैद्धांतिक निर्णयक्षमता (decidability) और अभिव्यंजक शक्ति (expressive power) को स्थापित करता है।
यह शोध पत्र ट्यूरिंग मशीनों को कार्यान्वित और सत्यापित करते हुए डेटा ऑटोनॉमस प्रोग्रामिंग भाषा AuDaLa की ट्यूरिंग पूर्णता (Turing completeness) स्थापित करता है, साथ ही इसकी व्यावहारिक अभिव्यक्ति क्षमता और पारंपरिक समानांतर भाषाओं के साथ इसके तालमेल को बढ़ाने के लिए विस्तार प्रस्तावित करता है।
यह शोध पत्र दो ऐसी श्रेणियों के बीच एक प्रतिवर्ती (contravariant) एडजंक्शन स्थापित करने के लिए बीजगणितीय और टोपोलॉजिकल विधियों का उपयोग करते हुए संक्रमण संरचनाओं (transition structures) की श्रेणियों की जांच करता है, जिसके परिणाम वस्तुओं और मोर्फिज्मों पर विशिष्ट टोपोलॉजिकल प्रतिबंधों के आधार पर भिन्न होते हैं।
यह शोधपत्र सत्यापन प्रक्रियाओं के रूप में "मशीनों" की अवधारणा प्रस्तुत करता है ताकि एक दुर्बल घातांकीय स्थान (weak exponential space) का निर्माण किया जा सके जो वास्तविक घातांकीय (true exponential) पर रिट्रैक्ट होता है, जिससे घातांकीयता (exponentiability) के लिए एक टोपोलॉजिकल स्पष्टीकरण प्राप्त होता है और कॉम्पैक्ट स्थानों पर सार्वभौमिक परिमाणीकरण (universal quantification) के विशुद्ध टोपोलॉजिकल संस्करण को सक्षम बनाया जा सके।
यह शोध पत्र टेम्पोरल लॉजिक सिंथेसिस फॉर्मेट (TLSF) का संस्करण 1.2 प्रस्तुत करता है, जो मानक LTL का एक विस्तार है जिसमें सेट्स और फंक्शन्स जैसे उच्च-स्तरीय कंस्ट्रक्ट्स, पैरामीटराइज्ड प्रॉब्लम फैमिलीज, और परिमित निष्पादन (finite executions) के लिए LTLf सिमेंटिक्स वाले नए ऑपरेटर्स शामिल हैं।
यह शोध पत्र ऑपरेशनल प्रपोजिशनल डायनेमिक लॉजिक (OPDL) प्रस्तुत करता है, जो एक सामान्यीकृत ढांचा है जो कार्यक्रमों को उनके ट्रेसेस (traces) से अलग करके और एक पैरामीटराइज्ड ऑपरेशनल सिमेंटिक्स का उपयोग करके समवर्तीता (concurrency) को मॉडल करने की पारंपरिक डायनेमिक लॉजिक की सीमाओं को दूर करता है, जिसे एक गैर-वेलफाउंडेड सीक्वेंट कैलकुलस (non-wellfounded sequent calculus) के लिए एक नवीन कट-एलिमिनेशन प्रमाण द्वारा समर्थित किया गया है।
यह शोधपत्र रिसोर्स-इंडेक्स्ड मोडैलिटीज़ के साथ टोपोलॉजिकल एविडेंस लॉजिक को विस्तारित करने के लिए सेमिरिंग-एनोटेटेड टोपोलॉजिकल स्पेस पेश करता है, जो विशिष्ट समय, स्मृति या ऊर्जा बजट बाधाओं के तहत एपिस्टेमिक अवस्थाओं के औपचारिक तर्क को सक्षम बनाता है और साथ ही सुदृढ़ और सुदृढ़ पूर्ण अभिलेखीयकरण (अक्सियोमैटाइजेशन) प्रदान करता है।
COBALT-TLA एक न्यूरो-सिम्बोलिक सत्यापन लूप है जो क्रॉस-चेन ब्रिज कमजोरियों, जिसमें अनप्रॉम्प्टेड अटैक क्लासेस भी शामिल हैं, को कुशलतापूर्वक खोजने के लिए एक LLM को TLA+ मॉडल चेकर के साथ एक स्वचालित फीडबैक चक्र में एकीकृत करता है, जो औपचारिक विनिर्देशों (फॉर्मल स्पेसिफिकेशन्स) के निर्माण को निर्देशित करने के लिए नियत त्रुटि ट्रेसेस (डिटरमिनिस्टिक एरर ट्रेसेस) का उपयोग करता है।