1116 पेपर
यह शोध पत्र GRAMPUS प्रस्तुत करता है, जो एक श्रेणीबद्ध मोडल टाइप थ्योरी (graded modal type theory) है जो क्वांटम पल्स शेड्यूल्स को औपचारिक रूप से निर्दिष्ट और तर्क देने के लिए टेम्पोरल ग्रेड्स (temporal grades) का उपयोग करता है, जो इसकी सुसंगतता (soundness) और पूर्णता (completeness) को स्थापित करने के लिए कैटेगोरिकल और सिंटैक्टिक मॉडल दोनों प्रदान करता है।
यह शोध पत्र सकारात्मक विशेषता वाले परिमित रूप से जनित क्रमविनिमेय वलयों (finitely generated commutative rings) पर रैखिक पुनरावृत्ति अनुक्रमों (linear recurrence sequences) के लिए स्कोलेम समस्या (Skolem Problem) की निर्णयक्षमता (decidability) को यह सिद्ध करके स्थापित करता है कि उनके शून्य समुच्चय (zero sets) -सामान्य समुच्चयों (p-normal sets) के प्रभावी रूप से गणनीय परिमित संघ (effectively computable finite unions) हैं, जो S-इकाई समीकरणों (S-unit equations) और गुणात्मक रूप से स्वतंत्र संख्याओं (multiplicatively independent numbers) पर रैखिक समीकरणों को हल करने में हालिया प्रगति का लाभ उठाते हैं।
यह शोध पत्र वेटेड मॉडल एन्यूमरेशन (WME) को एक विशिष्ट सॉल्वर-स्तरीय कार्य के रूप में प्रस्तुत करता है और पूरक CDCL-आधारित एल्गोरिदम पेश करता है जो भारित मॉडलों को कुशलतापूर्वक सूचीबद्ध करने के लिए क्रोनोलॉजिकल और नॉन-क्रोनोलॉजिकल बैकट्रैकिंग फ्रेमवर्क दोनों में वेट प्रोपेगेशन, प्रूनिंग और कॉन्फ्लिक्ट एनालिसिस को एकीकृत करते हैं।
यह शोध पत्र एब्स्ट्रैक्ट रिव्राइटिंग सिस्टम्स (Abstract Rewriting Systems) का अगडा (Agda) में एक रचनात्मक औपचारिकीकरण प्रस्तुत करता है जो मानक प्रमाणों से शास्त्रीय तर्क (classical logic) को हटा देता है, टर्मिनेशन (termination) और कन्फ्लुएंस (confluence) मानदंडों को परिष्कृत करता है, और लैम्ब्डा कैलकुलस (lambda calculus) के औपचारिकीकरण के माध्यम से इसकी प्रयोज्यता को प्रदर्शित करता है।
यह शोध पत्र एक नवीन भविष्यकालीन टेम्पोरल मार्किंग तकनीक का उपयोग करके अनुक्रमिक नेटवर्क (sequential networks) का निर्माण करके, डिस्क्रीट और डेंस दोनों प्रकार के समय व्यवहारों पर मेट्रिक टेम्पोरल लॉजिक के लिए एक कुशल और स्केलेबल ऑनलाइन मॉनिटरिंग फ्रेमवर्क प्रस्तावित करता है, जो मौजूदा दृष्टिकोणों की तुलना में बेहतर प्रदर्शन प्रदर्शित करता है।
यह शोध पत्र स्थापित करता है कि पुशडाउन मल्टी-एजेंट सिस्टम के लिए मॉड्यूल चेकिंग ATL विनिर्देशों (specifications) के लिए 2EXPTIME-पूर्ण है लेकिन ATL* विनिर्देशों के लिए 4EXPTIME-पूर्ण है, जो एक दुर्लभ मामला है जहाँ एक प्रारंभिक निर्णय समस्या की जटिलता त्रि-घातीय समय (triply exponential time) से अधिक है।
यह शोध पत्र ट्रांसफॉर्मेशन ऑटोमेटा का उपयोग करते हुए क्लीनी अलजेब्रा (Kleene Algebra) के लिए परिमित मॉडल गुण (finite model property) का एक नवीन, प्रारंभिक प्रमाण प्रस्तुत करता है, जो परिमित संबंधात्मक मॉडलों के सापेक्ष क्लीनी अलजेब्रा की पूर्णता को स्थापित करता है और पाल्का, प्रैट और कोज़ेन के पिछले परिणामों को समाहित करता है।
यह शोध पत्र प्रदर्शित करता है कि ऑटोमैटिक संरचनाओं में एक एकल सार्वभौमिक परिमाणक (यूनिवर्सल क्वांटिफायर) को हटाना स्वाभाविक रूप से दोहरे चरघातांकीय विस्फोट (डबली एक्सपोनेंशियल ब्लो-अप) की आवश्यकता रखता है, जो यह सिद्ध करता है कि परिणामी भाषा के लिए रिक्तता (एम्प्टीनेस) निर्धारित करने की समस्या EXPSPACE-पूर्ण है और बुची अंकगणित (ब्यूची अरिथमेटिक) के अंशों के लिए नए निम्नतम स्तर (लोअर बाउंड्स) स्थापित करता है।
यह शोध पत्र डबल पुशआउट ग्राफ ट्रांसफॉर्मेशन सिस्टम्स की समाप्ति सिद्ध करने के लिए वेटेड टाइप ग्राफ तकनीक की शक्ति को बढ़ाकर, इसे अन्य श्रेणियों में सामान्यीकृत करके और साहित्य में पाए जाने वाले विभिन्न DPO विस्तारों को समाहित करके इसे उन्नत करता है।
यह शोध पत्र यह स्थापित करता है कि ग्राफ़ के सेट CMSO-परिभाषित और संदर्भ-मुक्त (context-free) दोनों हैं यदि और केवल यदि वे सीमित ट्री-विड्थ (tree-width) वाले मान्यता प्राप्त (recognizable) सेट हैं, जिन्हें परिभाषा योग्य ट्रांसडक्शन (definable transductions) के माध्यम से व्युत्पत्ति वृक्षों (derivation trees) में पार्स किया जा सकता है, या परिभाषा योग्य ट्रांसडक्शन के तहत मान्यता प्राप्त ट्री सेट्स के इमेज हैं, जो ग्राफ भाषाओं के तार्किक अभिलक्षणों को इष्टतम ट्री अपघटन (tree decompositions) के निर्माण पर परिणामों के साथ एकीकृत करके किया गया है।