1092 पेपर
यह शोध पत्र एक मैकेनाइज्ड (mechanized) Isabelle/HOL प्रमाण प्रस्तुत करता है जो वैश्विक वित्तीय नियामक आवश्यकताओं के एक व्यापक मॉडल के विरुद्ध सात जेनेरिक लोकेल्स (generic locales) के इंस्टेंशिएशन का उपयोग करते हुए, बायज़ेंटाइन दोषों (Byzantine faults) के तहत क्रॉस-डोमेन नियामक अवस्था संरक्षण के लिए सुरक्षा और जीवंतता (liveness) दोनों गारंटियों को स्थापित करता है।
यह शोध पत्र एक त्सिटिन-समान (Tseitin-like) अनुवाद प्रस्तुत करता है जो मनमाने मीट्रिक टेम्पोरल सूत्रों को एक ऐसे लॉजिक प्रोग्राम खंड में कम करता है जो अतीत के ऑपरेटरों (past operators) तक सीमित है, जिससे मीट्रिक टेम्पोरल इक्विलिब्रियम लॉजिक में मात्रात्मक समय संबंधी बाधाओं के बारे में तर्क करने के लिए मौजूदा आंसर सेट प्रोग्रामिंग (ASP) सॉल्वरों का उपयोग करना सक्षम हो जाता है।
यह शोध पत्र संबंधपरक संरचनाओं (relational structures) पर प्रथम-क्रम परिभाषित संक्रियाओं (first-order definable operations) का सर्वेक्षण करता है, जो बैकवर्ड्स ट्रांसलेशन (Backwards Translation) और स्प्लिटिंग थ्योरम्स (Splitting Theorems) पर ध्यान केंद्रित करता है जो इनपुट गुणों के माध्यम से आउटपुट गुणों को व्यक्त करते हैं, जिसमें क्वांटिफायर-फ्री ऑपरेशंस (quantifier-free operations), मोड्यूलो काउंटिंग (modulo counting), और सीमित ट्री-विड्थ (tree-width) या क्लिक-विड्थ (clique-width) वाली संरचनाओं के लिए एल्गोरिद्मिक पहचान क्षमता (algorithmic recognizability) के विशिष्ट अनुप्रयोग शामिल हैं।
यह शोध पत्र ब्लॉक्स वर्ल्ड (Blocks World) और मिनीग्रिड (Minigrid) जैसे डोमेन में प्रभावी स्टेट-स्पेस एब्स्ट्रैक्शन के लिए डिक्लेरेटिव लॉजिकल रिप्रेजेंटेशन का लाभ उठाने हेतु रिलेशनल रिइन्फोर्समेंट लर्निंग को बढ़ाने के लिए CARCASS फ्रेमवर्क के एक आंसर-सेट प्रोग्रामिंग (ASP) कार्यान्वयन का प्रस्ताव और मूल्यांकन करता है।
यह शोध पत्र एक सैद्धांतिक संबंध स्थापित करता है जो यह दर्शाता है कि -रेगुलर गुणों को संतुष्ट करने वाली नीतियों के लिए वैल्यू फंक्शन (value functions), स्ट्रीट सुपरमार्टिंगेल प्रमाणपत्रों (Streett supermartingale certificates) को एनकोड करते हैं, जिससे औपचारिक सत्यापन (formal verification) और सुदृढीकरण लर्निंग (reinforcement learning) के बीच एक सेतु बनता है ताकि परिमित (finite), गणनीय अनंत (countably infinite) और निरंतर (continuous) अवस्था स्थानों में सिद्धांत-आधारित प्रमाण-संश्लेषण (principled certificate synthesis) को सक्षम किया जा सके।
यह शोध पत्र एक डिक्लेरेटिव डैलोग (Datalog) फ्रेमवर्क प्रस्तुत करता है जो जटिल समवर्ती सहयोगात्मक अनुप्रयोगों के व्यवस्थित विनिर्देशन, स्वचालित विश्लेषण और गुण-आधारित परीक्षण को सक्षम करने के लिए कॉन्फ्लिक्ट-फ्री रेप्लिकेटेड डेटा टाइप्स (CRDTs) को निष्पादन योग्य लॉजिक प्रोग्राम्स के रूप में मॉडल करता है।
यह शोध पत्र MSO-परिभाषित पैरिटी गेम्स (parity games) को हल करने और एकसमान मेमोरीलेस जीतने वाली रणनीतियों (uniform memoryless winning strategies) को व्युत्पन्न करने की एक विधि स्थापित करके अनंत अवस्था प्रणालियों (infinite state systems) के संश्लेषण का एक व्यवस्थित अध्ययन प्रस्तुत करता है।
यह शोधपत्र प्रथम-क्रम तर्क (First-Order Logic) के गार्डेड फ्रैगमेंट (Guarded Fragment) के लिए न्यूनतम मॉडल आकार पर एक इष्टतम द्वि-घातीय (doubly-exponential) ऊपरी सीमा के साथ परिमित मॉडल गुण (finite model property) स्थापित करने वाला एक नया संभाव्य प्रमाण प्रस्तुत करता है, जिसे तत्पश्चात डि-रैंडमाइज (derandomize) किया गया है और ट्रि-गार्डेड फ्रैगमेंट (Triguarded Fragment) तक विस्तारित किया गया है।
यह शोधपत्र मोनोटोनिक सिमेंटिक पाथ ऑर्डर्स और वेटेड पाथ ऑर्डर्स का एक सरल एकीकरण प्रस्तुत करता है, जो टर्म रीराइट सिस्टम्स की समाप्ति सिद्ध करने के लिए रिडक्शन ऑर्डर्स, रिडक्शन पेयर्स और ग्राउंड टोटल रिडक्शन ऑर्डर्स के रूप में उनके अनुप्रयोग को प्रदर्शित करता है।
यह शोध पत्र क्वांटाइज्ड सेटिंग्स में फीडफॉरवर्ड न्यूरल नेटवर्क को सत्यापित करने के लिए कम्प्यूटेशनल जटिलता परिदृश्य को स्थापित करता है, यह प्रदर्शित करते हुए कि लीनियर और बिट-वेक्टर दोनों विनिर्देशों के तहत फिक्स्ड अरिथमेटिक प्रिसिजन वाले नेटवर्क के लिए सत्यापन NP-कम्प्लीट रहता है, जबकि बिट-वेक्टर विनिर्देशों के तहत डायनामिकली क्वांटाइज्ड नेटवर्क के लिए नए अपर बाउंड प्रदान करता है।