1086 पेपर
यह शोधपत्र मेट्रिक इंटरवल टेम्पोरल लॉजिक (MITL) संतुष्टि के लिए एक नया, सरलीकृत दृष्टिकोण प्रस्तुत करता है जो एक शब्द (word) के साथ समय-बाधित दायित्वों को ट्रैक करता है और अनावश्यक दायित्वों को मर्ज करने के लिए एक तंत्र का उपयोग करता है, जिससे दायित्वों की एक सीमित संख्या सुनिश्चित होती है और क्षेत्रों (regions) पर आधारित एक प्रतीकात्मक प्रक्रिया सक्षम होती है।
यह शोध पत्र एक नवीन डोमेन-सैद्धांतिक प्रमाण तकनीक प्रस्तुत करता है जो नॉर्मलाइजेशन पर निर्भर किए बिना डिपेंडेंट टाइप सिस्टम के लिए डेफिनिशनल इनवर्जन गुणों को स्थापित करता है, जिससे इड्रिस (Idris) और लीन (Lean) जैसे नॉन-नॉर्मलाइजिंग सिस्टम के साथ-साथ टाइप-इन-टाइप (type-in-type) वाले सिस्टम का मेटा-थ्योरिटिक विश्लेषण सक्षम होता है।
यह शोध पत्र तार्किक प्रणालियों के लिए अर्थ का एक अंतर्निहित सिद्धांत प्रदान करने हेतु बेस-एक्सटेंशन सिमेंटिक्स (B-eS) और हाइलैंड-ओंग गेम सिमेंटिक्स के बीच एक पूर्णतः अमूर्त सहसंबंध स्थापित करता है, जिसे 4x4 सुडोकू के उदाहरण के माध्यम से स्पष्ट किया गया है।
यह शोध पत्र यह स्थापित करता है कि सिंक्रोनस परफेक्ट रिकॉल के तहत फाइनाइट बुची ऑटोमेटा पर व्याख्यायित, पास्ट (past) के साथ एपिस्टेमिक मेट्रिक टेम्पोरल लॉजिक के एजेंट-अल्टरनेशन-फ्री फ्रैगमेंट के लिए मॉडल चेकिंग, EXPSPACE-कम्प्लीट है, जो एक परिणाम है जिसे अविभेद्य इतिहासों की जटिलताओं को संभालने के लिए टेम्पोरल टेस्ट ऑटोमेटा को परफेक्ट-रिकॉल ऑब्जर्वर्स के साथ संयोजित करके प्राप्त किया गया है।
यह शोध पत्र क्वांटम कंप्यूटिंग गेट्स के लिए फोटोनिक सर्किट को संश्लेषित और अनुकूलित करने हेतु -वीकनिंग (weakening) SMT सॉल्वर dReal का उपयोग करने वाले एक टूल को प्रस्तुत करता है, जो गारंटीकृत इष्टतमता (optimality) प्रदान करता है और ज्ञात परिणामों को पुनरुत्पादित करके तथा गिवेंस रोटेशन गेट्स (Givens rotation gates) के लिए नए समाधानों की खोज करके अपनी प्रभावशीलता प्रदर्शित करता है।
यह शोधपत्र सहज बोधगम्य तर्कशास्त्र (intuitionistic logic) में एक प्रमाण-सिद्धांतिक विवरण प्रस्तुत करता है जो यह प्रदर्शित करता है कि धनात्मक पूर्णांकों का 1, अभाज्य और भाज्य में वर्गीकरण सीमित खोजों (bounded searches) के माध्यम से निर्णायक है, जिससे एक पुनरावर्ती छलनी (recursive sieve), मॉड्यूलर रद्दीकरण (modular cancellation) का एक लक्षणण, और इस बात के बीच एक अंतर स्पष्ट होता है कि हाइटिंग अंकगणित (Heyting Arithmetic) आंतरिक रूप से क्या सिद्ध करता है बनाम क्या प्राकृतिक संख्याओं की मानक व्याख्या पर निर्भर करता है।
यह शोधपत्र Rzk को प्रस्तुत करता है, जो -श्रेणियों (categories) के बारे में सिंथेटिक तर्क (synthetic reasoning) को सक्षम करने के लिए रीहल और शुलमैन के सिमपलीशियल टाइप थ्योरी के एक परिष्कृत, कम्प्यूटेशनल वेरिएंट को लागू करने वाला एक व्यावहारिक प्रूफ़ असिस्टेंट है, जबकि मूल सिद्धांत के सापेक्ष इसकी निष्ठा (faithfulness) और संरक्षणशीलता (conservativity) को स्थापित करता है और इसके उपयोग एवं कार्यान्वयन पर एक ट्यूटोरियल प्रदान करता है।
यह शोध पत्र FLEX प्रस्तुत करता है, जो सत्यापित Lean प्रमेय सिद्धकर्ता (theorem prover) में कार्यान्वित एक मौलिक 'कन्स्ट्रेंड हॉर्न क्लॉज' (Constrained Horn Clause) सॉल्वर है, जो विश्वसनीय कंप्यूटिंग बेस को कर्नेल तक सीमित करता है और SMT की अभिव्यक्ति सीमाओं को पार करने के लिए Lean के प्रमाण पारिस्थितिकी तंत्र (proof ecosystem) का लाभ उठाता है और उच्च सफलता दर के साथ निम्न-स्तरीय सिस्टम कोड को स्वचालित रूप से सत्यापित करता है।
यह शोध पत्र एक नवीन प्री-एक्स्पेक्टेशन (pre-expectation) ढांचे को पेश करके क्वांटम वीकेस्ट प्रीकंडिशन्स (quantum weakest preconditions) पर पुनर्विचार करता है, जो रिवॉर्ड्स और संभावित रूप से अनंत अपेक्षित रनटाइम वाले क्वांटम प्रोग्रामों के बारे में तर्क करने के लिए अपेक्षित रनटाइम विश्लेषण हेतु सक्षम बनाता है, जिसमें किसी ऊपरी सीमा की आवश्यकता नहीं होती है।
यह शोधपत्र एक आधारभूत तर्क (base logic) के भीतर इफेक्ट हैंडलर्स (effect handlers) को लागू करके विस्तार योग्य प्रोग्राम लॉजिक्स बनाने का एक दृष्टिकोण प्रस्तावित करता है ताकि कंकरेंसी (concurrency) और क्रैश रिकवरी (crash recovery) जैसे जटिल व्यवहारों को मॉडल किया जा सके, जिससे एक मॉड्यूलर और पुन: प्रयोज्य तरीके से अभिव्यंजक तर्क नियमों (reasoning rules) और रिलेशनल रिफाइनमेंट्स (relational refinements) का व्युत्पन्न सक्षम हो सके।