1109 पेपर
यह शोध पत्र द्वितीय-क्रम क्वांटिफायर एलिमिनेशन (second-order quantifier elimination) के लिए सैचुरेशन-आधारित SCAN एल्गोरिदम का विस्तार उन द्वितीय-क्रम क्वांटिफायर्स के लिए विटनेस (witnesses) की गणना करने हेतु करता है जो तार्किक रूप से समतुल्य प्रथम-क्रम सूत्रों (first-order formulas) को उत्पन्न करते हैं और इस विधि का एक प्रोटोटाइप कार्यान्वयन प्रस्तुत करता है।
यह शोध पत्र लीनियर लॉजिक के वेटेड रिलेशनल सिमेंटिक्स का उपयोग करते हुए, उनके संबंधित जनरेटिंग फंक्शन्स के बीजगणितीय (algebraic) होने को सिद्ध करके, एफ़ाइन सिस्टम्स का विस्तार करने वाले प्रोबेबिलिस्टिक हायर-ऑर्डर रिकर्सन स्कीम्स (PHORS) के एक वर्ग के लिए 'ऑलमोस्ट शुअर टर्मिनेशन' की निर्णयक्षमता (decidability) स्थापित करता है।
यह शोध पत्र एक विस्तारित न्यूरो-सिम्बोलिक ढांचे को प्रस्तुत करता है जो एक मेटा-स्तरीय संश्लेषण और सत्यापन पाइपलाइन को एकीकृत करता है, जो उच्च-स्तरीय कानूनी और सुरक्षा सिद्धांतों को सुरक्षा-महत्वपूर्ण स्वायत्त प्रणालियों के लिए औपचारिक रूप से सत्यापित, न्यूनतम कारण नियमों में अनुवादित करने के लिए लार्ज लैंग्वेज मॉडल्स का लाभ उठाता है।
यह शोध पत्र धनात्मक परिमेय सिमेंटिक संख्यांकन प्रणालियों (positive rational Semantic Numeration Systems) को प्रस्तुत करता है, कार्डिनल सिमेंटिक ऑपरेटरों के लिए उनके कैरी (carry) और शेषफल (remainder) संचालन को परिभाषित करता है, उदाहरणों के माध्यम से उनके गतिक गुणों का विश्लेषण करता है, और आंशिक पूर्णांक सिमेंटिक संख्यांकन प्रणालियों (partial integer Semantic Numeration Systems) के लिए एक प्रारंभिक ढांचे का प्रस्ताव करता है।
यह शोध पत्र अनंत डेटा पर कार्य करने वाले फलनों के स्कॉट-ओपन (Scott-open) इनपुट-आउटपुट गुणों को सत्यापित करने के लिए एक सुदृढ़ और पूर्ण फाइनाइटरी रिफाइनमेंट टाइप सिस्टम प्रस्तुत करता है, जो एब्राम्स्की के डोमेन थ्योरी इन लॉजिकल फॉर्म (Domain Theory in Logical Form) और रियलाइज़ेबिलिटी (realizability) के बीच सेतु बनाने के लिए स्कॉट डोमेन की स्पेक्ट्रल प्रकृति और तार्किक ध्रुवीयता (logical polarities) का लाभ उठाता है।
यह शोध पत्र ATL-D और इसके ज्ञान-जागरूक विस्तार (knowledge-aware extension) ATEL-D को प्रस्तुत करता है ताकि मल्टी-एजेंट सिस्टम में कार्यों के गतिशील अनुदान (granting) और प्रतिधारण (revoking) को मॉडल किया जा सके, साथ ही उनकी अभिव्यंजना शक्ति (expressivity), मानदण्डिक प्रणालियों (normative systems) के साथ संबंध और कम्प्यूटेशनल जटिलता का विश्लेषण किया जा सके।
यह शोध पत्र क्वांटम बेयसियन नेटवर्क के लिए एक संरचनात्मक ढांचे (compositional framework) को प्रस्तुत करता है जो एक लीनियर लॉजिक प्रूफ-नेट टाइपिंग अनुशासन का उपयोग करके शास्त्रीय और क्वांटम कारण संबंधी तर्क (causal reasoning) को एकीकृत करता है, जो शास्त्रीय कारणों के लिए मानक बेयसियन अर्थविज्ञान और विशुद्ध रूप से क्वांटम प्रणालियों के लिए टेंसर नेटवर्क को पुनर्प्राप्त करता है।
यह शोधपत्र यह स्थापित करता है कि अनंत वृक्षों (infinite trees) पर प्रथम-क्रम तर्क (First-Order Logic), \PolPCTL और \CTLsf के अनुरूप हिचकिचाते वृक्ष ऑटोमेटा (hesitant tree automata) के दो वर्गों द्वारा सटीक रूप से कैप्चर किया जाता है, जिससे एक समान ऑटोमेटा-सैद्धांतिक लक्षण वर्णन प्राप्त होता है और यह प्रकट होता है कि प्रथम-क्रम परिभाषितता (first-order definability) मौलिक रूप से प्रत्येक शाखा के साथ सुरक्षा (safety) या सह-सुरक्षा (co-safety) गुणों तक ही सीमित है।
यह शोधपत्र उच्च-क्रम तार्किक रूप से बाधित टर्म रीराइटिंग सिस्टम्स (Logically Constrained Term Rewriting Systems) के लिए बाउंडेड रीराइटिंग इंडक्शन (Bounded Rewriting Induction) के भीतर ऑटोमैटिकली इंडक्शन हाइपोथीसिसिस (induction hypotheses) उत्पन्न करने के लिए एक नया टेम्पलेट-आधारित दृष्टिकोण प्रस्तुत करता है, जो विशिष्ट प्रोग्रामिंग कंस्ट्रक्ट्स को उच्च-क्रम फंक्शन इंस्टेंस के रूप में पहचानकर उन प्रोग्राम इक्विवेलेंसेस (program equivalences) को सिद्ध करने में सक्षम बनाता है जो पहले अप्राप्य थे।
यह शोध पत्र एक नए DPLL()-आधारित SMT सॉल्वर को प्रस्तुत करता है जो प्राइम फील्ड्स पर बहुपद समीकरणों की संतुष्टि (satisfiability) को कुशलतापूर्वक निर्धारित करने के लिए कई मॉड्यूल को व्यवस्थित करता है, जो मौजूदा अत्याधुनिक उपकरणों की तुलना में ज़ीरो-नॉलेज प्रूफ प्रोटोकॉल को सत्यापित करने में बेहतर प्रदर्शन प्रदर्शित करता है।