1115 पेपर
यह अध्ययन प्रकट करता है कि जबकि ट्रांसफार्मर मॉडल स्केलिंग के माध्यम से कम-आयामी ग्रिड जैसी संरचनाओं पर ट्रांजिटिव कनेक्टिविटी को प्रभावी ढंग से सीख और सामान्यीकृत कर सकते हैं, वे कई विच्छेदित घटकों या उच्च-आयामी संरचनाओं वाले जटिल ग्राफों पर ऐसा करने में संघर्ष करते हैं।
यह शोध पत्र APPL को प्रस्तुत करता है, जो एक एकीकृत होअर-शैली (Hoare-style) का तर्क है जो एक लचीले अर्थपूर्ण ढांचे (semantic framework) पर आधारित है जो मानक, त्रुटिपूर्ण (incorrectness), और हाइपर लॉजिक्स को समाहित करता है और साथ ही मूर्त (concrete) और अमूर्त (abstract) दोनों प्रोग्राम गुणों के लिए सुदृढ़ और अपेक्षाकृत पूर्ण प्रमाण प्रणालियाँ प्रदान करता है।
यह शोध पत्र पिछले स्केलेबिलिटी (scalability) की सीमाओं को दूर करने के लिए NAUTY के साथ रिकर्सिव कैनोनिकल लेबलिंग को एकीकृत करते हुए एक नवीन SAT-आधारित ऑर्डरली जनरेशन फ्रेमवर्क प्रस्तुत करता है, जो आयाम 3 में छोटे कोचेन-स्पेक्टर (Kochen-Specker) सेट्स के पहले व्यापक गणना (exhaustive enumeration) को सक्षम बनाता है और यह सत्यापित करता है कि श्यूट (Schütte) का 33-रे सेट, पूर्ण 25-रे स्टेट-इंडिपेंडेंट कॉन्टेक्स्टुअलिटी सेट को समाहित करने वाला सबसे छोटा सेट है।
यह विस्तारित शोधपत्र मानव बोध को बढ़ाने के लिए स्पष्ट-अवस्था मॉडलों (explicit-state models) पर CTL साक्षी (witnesses) और प्रति-उदाहरणों (counterexamples) को विज़ुअलाइज़ करने के लिए एक औपचारिक मॉडल प्रस्तुत करता है, जो प्रत्येक टेम्पोरल ऑपरेटर के लिए न्यूनतम साक्ष्य का अभिलक्षणन और एक ठोस कार्यान्वयन के साथ-साथ सभी परिणामों के प्रमाण भी प्रदान करता है।
यह शोध पत्र मोडल बीजगणितों (modal algebras) और संबंधात्मक स्थानों (relational spaces) के बीच स्टोन-प्रकार की द्वैतताओं (Stone-type dualities) के एक परिवार को स्थापित करता है, यह प्रदर्शित करते हुए कि विभिन्न रूपान्तरण परिभाषाएँ (morphism definitions) बिंदु निर्माणों (point constructions) को कैसे प्रभावित करती हैं और अर्ध-सतत संबंध (semicontinuous relations) मोडल अभिधारणाओं (modal axioms) और संबंधात्मक गुणों (relational properties) के बीच पत्राचार को कैसे सरल बनाते हैं।
यह शोध पत्र प्राइमल-डुअल एल्गोरिदम विश्लेषण को औपचारिक रूप से सत्यापित करने के लिए एक Isabelle/HOL फ्रेमवर्क और लाइब्रेरी विकसित करने की एक चल रही पहल को रेखांकित करता है, जो हंगेरियन मेथड जैसे शास्त्रीय मिलान एल्गोरिदम और एडवर्ड्स (Adwords) एल्गोरिदम जैसे आधुनिक दृष्टिकोणों दोनों के औपचारिकीकरण के माध्यम से अपने अनुप्रयोग को प्रदर्शित करता है।
यह शोध पत्र यह स्थापित करता है कि अनएनोटेटेड (unannotated) डेटाबेस के लिए पहले से ज्ञात कंजंक्टिव क्वेरी उत्तरों तक प्रत्यक्ष पहुँच की सूक्ष्म-स्तरीय जटिलता (fine-grained complexity) की शर्तें, एग्रीगेशन और सेमिरिंग एनोटेशन वाली क्वेरीज़ (बशर्ते एनोटेशन को क्रम से बाहर रखा जाए) तक विस्तारित होती हैं, साथ ही यह काउंट-डिस्टिंक्ट (count-distinct) एग्रीगेशन के लिए नई सुगमता (tractability) की शर्तों को व्युत्पन्न करता है और क्रम में एग्रीगेट मानों को शामिल करने या विशिष्ट सेमिरिंग गुणों का उपयोग करने के प्रभाव का विश्लेषण भी करता है।
यह शोध पत्र "इंडक्टिव प्रूफ डिकंपोजिशन" (inductive proof decomposition) प्रस्तुत करता है, जो एक संवादात्मक कार्यप्रणाली है जो मानव सत्यापनकर्ताओं को एक इंडक्टिव प्रूफ ग्राफ को क्रमिक रूप से बनाने, काउंटरएग्जम्पल्स को स्थानीयकृत करने और अप्रासंगिक स्टेट को स्लाइस करने के माध्यम से जटिल वितरित प्रोटोकॉल के लिए सुरक्षा प्रमाणों के निर्माण में मार्गदर्शन करती है, ताकि पूर्णतः स्वचालित सत्यापन उपकरणों की सीमाओं को दूर किया जा सके।
यह शोध पत्र यह सिद्ध करता है कि कंजर्वेटिव पेट्री नेट्स (conservative Petri nets) के लिए स्ट्रक्चरल लाइवनेस (structural liveness) EXPSPACE-पूर्ण है, क्योंकि यह स्थापित करता है कि स्ट्रक्चरली लाइव कंजर्वेटिव नेट्स के लिए मिनिमल लाइव मार्किंग्स (minimal live markings), नेट के आकार के दोगुने एक्सपोनेंशियल (doubly exponential) फलन द्वारा सीमित हैं।
यह शोध पत्र एक भारित मॉडल-आधारित ज्ञानमीमांसीय तर्क (एपिस्टेमिक लॉजिक) ढांचे को प्रस्तुत करता है जो ज्ञान प्राप्ति को 'अपस्किलिंग' और विस्मृति को 'डाउनस्किलिंग' के रूप में गतिशील रूप से मॉडल करने के लिए एक "ज्ञान संबंधी कौशल" (एपिस्टेमिक स्किल्स) मीट्रिक का उपयोग करता है, साथ ही समूह ज्ञान, बोधगम्यता, विस्मृति और प्रणाली की गणनात्मक जटिलता का भी विश्लेषण करता है।