1090 पेपर
यह शोध पत्र गतिशील नेटवर्क में रैंडमाइज्ड वितरित एल्गोरिदम के विश्लेषण के लिए एक संभाव्य एपिस्टेमिक लॉजिक फ्रेमवर्क प्रस्तुत करता है, जो वर्घेसे-लिंच एल्गोरिदम का एक औपचारिक ज्ञान-सैद्धांतिक उपचार और एक सुदृढ़, सटीक निचला स्तर (लोअर बाउंड) प्रदान करने के लिए समन्वित हमले की समस्या (कोऑर्डिनेटेड अटैक प्रॉब्लम) पर इसे लागू करता है।
यह शोध पत्र रिएक्टिव सिंथेसिस विनिर्देशों (specifications) को विघटित करने के लिए DecomposeContract एल्गोरिदम का एक कठोर सिमेंटिक विश्लेषण प्रदान करता है, एक प्रति-उदाहरण (counterexample) के माध्यम से इसकी अपूर्णता की पहचान करता है, और एक परिष्कृत, पूर्ण विघटन प्रक्रिया प्रस्तावित करता है जो स्वतंत्र चर सेटों (independent variable sets) की पहचान करने के लिए मॉडल चेकिंग का लाभ उठाती है।
यह शोध पत्र "स्वैप ग्राफ्स" (swap graphs) के माध्यम से बूलियन संतुष्टि (Boolean satisfiability) में एक गैर-तुच्छ न्यूनीकरण (non-trivial reduction) पेश करके NP-पूर्ण पोसेट कवर (poset cover) समस्या के लिए एक नवीन दृष्टिकोण प्रस्तुत करता है, जो Z3 जैसे आधुनिक SAT सॉल्वर का उपयोग करके उचित यूनिवर्स आकारों के लिए कुशल समाधान सक्षम बनाता है।
यह शोध पत्र प्रदर्शित करता है कि सीमित रैखिक क्लिक-चौड़ाई (bounded linear clique-width) वाले टूर्नामेंट्स के लिए, प्रथम-क्रम ट्रांसडक्शन (first-order transductions) सीमित-चौड़ाई वाले क्लिक-विघटन (bounded-width clique-decompositions) उत्पन्न करने के लिए पर्याप्त हैं, जिससे इस संदर्भ में CMSO और अस्तित्व संबंधी MSO लॉजिक्स के बीच समानता स्थापित होती है।
यह शोधपत्र 'आइडियल सिचुएशंस' (ideal situations) की अवधारणा पर निर्भर हुए बिना, यह मॉडल करने के लिए कि कैसे ऐसे कार्य निरंतर दायित्व उत्पन्न करते हैं, रीटर (Reiter) के बुनियादी एक्शन थ्योरीज और रिग्रेशन ऑपरेटर का विस्तार करके, दायित्व-उत्पादक कार्यों के लिए फ्रेम प्रॉब्लम (frame problem) हेतु एक सरलीकृत सिचुएशन कैलकुलस (Situation Calculus) समाधान प्रस्तुत करता है।
यह शोध पत्र DEC को प्रस्तुत करता है, जो एक ऐसा ढांचा है जो ज्ञान ग्राफ (knowledge graphs) में प्रोवेनेंस (provenance) की व्याख्या एपिस्टेमिक स्टैंड्स (epistemic stance) के संकेतकों के रूप में करता है ताकि एट्रिब्यूटेड दावों को "कॉग्निटिव वर्ल्ड्स" (cognitive worlds) में व्यवस्थित किया जा सके, जिससे असहमति और परिकल्पनाओं को विसंगतियों में बदले बिना उन पर सिद्धांतपूर्ण तर्क करना सक्षम हो सके।
यह शोध पत्र एक GPU-त्वरित ढांचे को प्रस्तुत करता है जो व्यापक स्तर पर पूर्ण मोडल फॉर्मूला मूल्यांकन और काउंटरमॉडल प्रमाणन करने के लिए परिमित क्रिप्के सिमेंटिक्स (Kripke semantics) को बिटमास्क के रूप में एनकोड करता है, जो रिफ्यूटेबिलिटी (refutability) पर कड़े बंधों को प्रकट करता है, सिमेंटिक मिराज (semantic mirages) को संश्लेषित करता है, और ग्राफिक्स-समर्थित सिमेंटिक अन्वेषण को सक्षम बनाता है।
यह शोध पत्र 1986 के ICON यूक्लिडियन डोमेन एल्गोरिदम का एक पूर्ण लीन 4 (Lean 4) औपचारिक रूपान्तरण प्रस्तुत करता है, जो मूल बेंचमार्क परिणामों को संरक्षित करते हुए मुख्य प्रक्रियाओं के लिए मशीन-चेक किए गए प्रमाण प्रदान करने हेतु गणितीय परिभाषाओं, गणनीय कार्यान्वयन और लेगेसी आउटपुट पुनरुत्पादन को अलग करता है।
यह शोध पत्र तार्किक अभिव्यक्तियों और डेटाबेस प्रश्नों को सरल बनाने के लिए क्रेग इंटरपोलेशन (Craig interpolation) और बेथ डेफिनैबिलिटी (Beth definability) के अनुप्रयोगों का अवलोकन करता है, जो प्रभावी एल्गोरिदम, मॉडल-सैद्धांतिक संरक्षण प्रमेयों (model-theoretic preservation theorems) के साथ संबंधों, और डेटाबेस हितों के अनुरूप तैयार किए गए इंटरपोलेशन रूपों के विकास पर नए दृष्टिकोण प्रस्तुत करता है।
यह शोध पत्र प्रकट करता है कि जहाँ लार्ज लैंग्वेज मॉडल्स औपचारिक तर्क ढाँचों के माध्यम से कानूनी एंटेलमेंट कार्यों में उच्च सटीकता प्राप्त करते हैं, वहीं उनका प्रदर्शन अक्सर "स्कोप लॉन्ड्रिंग" जैसे व्यवस्थित विफलता मोडों के कारण अविश्वसनीय होता है, जहाँ मॉडल वास्तव में अंतर्निहित प्रतीकात्मक सॉल्वर को निष्पादित किए बिना तार्किक रूप से असंगत निष्कर्ष उत्पन्न करते हैं।