1115 पेपर
यह शोधपत्र कार्मो और जोन्स की सशर्त दायित्वों (conditional obligations) के लिए हालिया स्वयंसिद्ध प्रणाली (axiom system) की आलोचना एक सीमित प्रकार के 'डीओन्टिक एक्सप्लोजन' (deontic explosion) को प्रदर्शित करते हुए करता है, और साथ ही उनके सबसे सशक्त 1997 के तंत्र के सभी संतुष्ट मॉडलों का एक एकल वर्जित संभव विश्व (forbidden possible world) के संदर्भ में सकारात्मक वर्गीकरण प्रस्तुत करता है।
यह शोध पत्र समानता और परिवर्तनशील डोमेन स्थितियों वाले परिमाणित मोडल लॉजिक (quantified modal logics) के एक व्यापक वर्ग के लिए पहले सुसंगत (sound) और पूर्ण (complete), कट-मुक्त (cut-free) नेस्टेड सीक्वेंट सिस्टम (nested sequent systems) को प्रस्तुत करता है, जो जटिल फ्रेम गुणों को संभालने के लिए सिग्नेचर-आधारित नियमों और व्याकरण-पैरामीटराइज्ड रीचैबिलिटी नियमों का उपयोग करते हुए इनवर्टिबिलिटी (invertibility) और सिंटैक्टिक कट-एलिमिनेशन (syntactic cut-elimination) जैसे प्रमुख प्रमाण-सैद्धांतिक गुणों को सिद्ध करते हैं।
यह शोध पत्र फॉक्सट्रॉट (Foxtrot) को प्रस्तुत करता है, जो पहला उच्च-क्रम पृथक्करण तर्क (higher-order separation logic) है जो उन्नत समवर्ती और संभाव्यता तर्क सिद्धांतों, जिसमें आइरिस (Iris) ढांचे के भीतर चयन के स्वयंसिद्ध (axiom of choice) पर एक नवीन निर्भरता शामिल है, को एकीकृत करके स्थानीय अवस्था वाले उच्च-क्रम समवर्ती संभाव्य कार्यक्रमों के लिए प्रासंगिक परिशोधन (contextual refinement) के मशीनीकृत प्रमाण को सक्षम बनाता है।
यह शोधपत्र प्रदर्शित करता है कि मौलिक अनुकूलन एम्बेडिंग (optimization embeddings), जिन्हें मूल रूप से मिश्रित-पूर्णांक प्रोग्रामिंग (mixed-integer programming) के लिए डिज़ाइन किया गया था, CNF सूत्रों को एक साझा द्विपक्षीय ग्राफ प्रतिनिधित्व (bipartite graph representation) में मैप करके अनसुपरवाइज्ड बूलियन सैटिस्फिएबिलिटी (SAT) कार्यों में सीधे स्थानांतरित किए जा सकते हैं, जिससे बिना किसी आर्किटेक्चरल परिवर्तन या सुपरवाइज्ड फाइन-ट्यूनिंग के इंस्टेंस क्लस्टरिंग और वितरण पहचान सक्षम होती है।
यह शोध पत्र \vmtlc टूल में कार्यान्वित एक काउंटरएग्जांपल-गाइडेड लर्निंग फ्रेमवर्क प्रस्तुत करता है जो जटिल लाइब्रेरीज़ का उपयोग करने वाले क्लाइंट प्रोग्रामों के सत्यापन को स्वचालित करता है, जो ऐसे मॉड्यूलर या कॉन्टेक्स्टुअल कॉन्ट्रैक्ट्स को संश्लेषित करता है जो क्लाइंट की शुद्धता सिद्ध करने के लिए पर्याप्त हैं और एक टेस्टिंग इंजन द्वारा मान्य भी हैं।
यह शोधपत्र यह प्रदर्शित करके निगमनात्मक स्रोतों (deductive sources) के लिए हानिपूर्ण संपीड़न (lossy compression) की मौलिक सीमाओं को स्थापित करता है कि जब निष्ठा (fidelity) को प्रतीक-वार समानता के बजाय तार्किक समापन (logical closure) के संरक्षण द्वारा मापा जाता है, तो दर-विकृति फलन (rate-distortion function) विशेष रूप से स्रोत के अपरिहार्य मूल (irredundant core) पर निर्भर करता है, जिससे अनावश्यक परिणाम संपीड़न दक्षता के लिए अदृश्य हो जाते हैं।
यह शोध पत्र रैंक-वन पॉलीमोर्फिक -कैल्कुलस टर्म्स के लिए पूर्ण और न्यूनतम टाइप एनोटेशन का एक औपचारिक मेटाथ्योरिटिकल विवरण और Isabelle/HOL मेकेनाइजेशन प्रस्तुत करता है, जिसे एक सहयोगात्मक वर्कफ़्लो के माध्यम से विकसित किया गया है जहाँ मानव और एआई एजेंट स्वतंत्र रूप से प्रमाण (proofs) उत्पन्न करते हैं जिन्हें बाद में मानव-निर्देशित एआई हस्तक्षेपों के साथ ऑटोफॉर्मलाइज और सामान्यीकृत किया जाता है।
यह शोध पत्र SATFuL प्रस्तुत करता है, जो फजी लॉजिक्स (fuzzy logics) के लिए एक नवीन SAT सॉल्वर है जो विभिन्न फजी लॉजिक सिस्टम्स में साउंडनेस (soundness), पूर्णता (completeness) और व्यापक प्रयोज्यता प्राप्त करने के लिए मिक्स्ड-इंटीजर नॉन-लीनियर प्रोग्रामिंग (MINLP) का लाभ उठाता है, जो मौजूदा अत्याधुनिक उपकरणों के तुलनीय या उनसे बेहतर प्रदर्शन प्रदर्शित करता है।
यह शोधपत्र प्रदर्शित करता है कि सौम्य परिस्थितियों के अंतर्गत, किसी योगात्मक सममित मोनॉइडल श्रेणी (additive symmetric monoidal category) पर कोई भी अवकल मोडैलिटी (differential modality), स्वाभाविक रूप से एक -फिल्टर्ड अवकल मोडैलिटी को प्रेरित करती है जहाँ मोर्फिज्म (morphisms) सीमित डिग्री वाले बहुपद मानचित्रों (polynomial maps) के अनुरूप होते हैं, जो उनके -वें अवकलज के शून्य होने द्वारा अभिलक्षित होते हैं।
यह शोध पत्र QBF गैलरी 2023 प्रस्तुत करता है, जो इस श्रृंखला में अंतिम मूल्यांकन कार्यक्रम है, जो एक नया समेकित बेंचमार्क सेट पेश करता है और QBF अनुसंधान एवं बेंचमार्किंग की भविष्य की दिशा पर चर्चा करते हुए अत्याधुनिक सॉल्वरों का तुलनात्मक विश्लेषण प्रदान करता है।