1105 पेपर
यह शोध पत्र मौजूदा बेंचमार्क की सीमाओं को दूर करने के लिए प्रमाणित रूप से ज्ञात ग्राउंड-ट्रुथ लेबल वाले न्यूरल नेटवर्क सत्यापन उदाहरण उत्पन्न करने के लिए एक फ्रेमवर्क पेश करता है, जो एक नए "डिफिकल्टी प्रोफाइल" मीट्रिक के माध्यम से विवरक (verifier) बग्स की खोज और विफलता मोड के व्यवस्थित विश्लेषण को सक्षम बनाता है।
यह शोध पत्र यह स्थापित करता है कि गणनीय लेबल वाले रैखिक क्रमों (countable labelled linear orders) पर दिए गए मोनैडिक सेकंड-ऑर्डर (MSO) सूत्र के लिए -आयामी पुनर्रचना (reparameterization) को स्वीकार करने की निर्धारितता (decidability) क्या है, जिससे यह सिद्ध होता है कि ऐसी किसी भी व्याख्या योग्य संरचना को समान रूप से एक -आयामी बिंदु व्याख्या (point interpretation) के रूप में निरूपित किया जा सकता है।
यह शोध पत्र प्रदर्शित करता है कि बाउंडेड अंकगणित सिद्धांत , यहाँ तक कि जब इसे सभी सूत्रों के लिए पिजनहोल सिद्धांत के साथ संवर्धित किया जाता है, फिर भी परिमित अंतरालों पर सख्त रैखिक क्रमों के लिए न्यूनीकरण सिद्धांत को सिद्ध करने में अपर्याप्त है।
यह शोध पत्र लॉजिक ऑफ हाइपोथीसिसिस (LoH) को प्रस्तुत करता है, जो एक नवीन न्यूरोसिम्बोलिक फ्रेमवर्क है जो प्रपोज़िशनल लॉजिक को एक सीखने योग्य 'चॉइस ऑपरेटर' के माध्यम से विस्तारित करके हस्तनिर्मित नियमों और डेटा-संचालित शिक्षण को एकीकृत करता है, जिसे डिफरेंशिएबल फजी लॉजिक में संकलित किया गया है, जिससे प्रदर्शन में बिना किसी कमी के लचीले ज्ञान एकीकरण और असतत बूलियन तर्क (डिस्क्रीट बूलियन रीजनिंग) को सक्षम बनाया जा सके।
यह शोधपत्र प्रदर्शित करता है कि फिक्स्ड-प्रिसिजन ट्रांसफॉर्मर (fixed-precision transformers) स्वाभाविक रूप से लीनियर टेम्पोरल लॉजिक (linear temporal logic), रिकरेंट न्यूरल नेटवर्क्स (recurrent neural networks) और फाइनाइट ऑटोमेटा (finite automata) की तुलना में घातीय रूप से अधिक संक्षिप्त हैं, एक ऐसा गुण जो एम्प्टीनेस (emptiness) और इक्विवेलेंस (equivalence) जैसी मौलिक सत्यापन समस्याओं को EXPSPACE-कम्पलीट बनाता है।
यह शोधपत्र डायनामिक हाइपरसीक्वेंट्स (dynamic hypersequents) प्रस्तुत करता है, जो पब्लिक अनाउंसमेंट लॉजिक (Public Announcement Logic) के लिए हाइपरसीक्वेंट कैलकुली का विस्तार करने वाला एक नवीन प्रमाण-सिद्धांतिक ढांचा है, जो एपिस्टेमिक अपडेट्स की गतिशीलता को सफलतापूर्वक कैप्चर करता है और संरचनात्मक नियम ग्राह्यता (structural rule admissibility), नियम व्युत्क्रमणीयता (rule invertibility) और सिंटैक्टिक कट-उन्मूलन (syntactic cut-elimination) जैसे प्रमुख गुणों को स्थापित करता है।
यह शोध पत्र यह स्थापित करता है कि जब लक्ष्य उपसमष्टि (target subspace) का आयाम लघुगणकीय (logarithmic) होता है, तो ऑर्बिट समस्या (Orbit Problem) एक NP^RP जटिलता सीमा के साथ निर्णायक (decidable) होती है, जबकि यह सिद्ध करता है कि जब लक्ष्य उपसमष्टि का आयाम रैखिक (linear) होता है, तो यह समस्या लंबे समय से खुले स्केलेम समस्या (Skolem Problem) जितनी ही कठिन हो जाती है।
यह शोध पत्र कोफोला (Kofola) का परिचय देता है, जो एक कुशल और सुदृढ़ उपकरण है जो अनुकूलित पूरक (complementation) और समावेशन जाँच के लिए बुची ऑटोमेटा (Büchi automata) को स्ट्रॉन्गली कनेक्टेड कंपोनेंट्स में विघटित करने हेतु एक मॉड्यूलर फ्रेमवर्क का उपयोग करता है, जो ऑन-द-फ्लाई एम्प्टीनेस चेकिंग और नई ह्यूरिस्टिक्स के माध्यम से अत्याधुनिक उपकरणों की तुलना में बेहतर प्रदर्शन प्रदर्शित करता है।
यह शोध पत्र एक बड़े BMC बेंचमार्क का विश्लेषण करके औद्योगिक SAT इंस्टेंस पर व्यवस्थित स्केलिंग अध्ययनों की कमी को संबोधित करता है, यह प्रदर्शित करते हुए कि हाल ही में प्रस्तावित "प्रूफडोर" (proofdoor) पैरामीटर—जो इंटरपुलेंट्स के एक अनुक्रम का प्रतिनिधित्व करता है—सफलतापूर्वक सॉल्वर प्रदर्शन स्केलेबिलिटी की व्याख्या करता है जहाँ पारंपरिक संरचनात्मक पैरामीटर विफल हो जाते हैं।
यह शोधपत्र गैर-वेलफाउंडेड (non-wellfounded) प्रमाण प्रणालियों के लिए एक को-अल्जेब्रिक ढांचा स्थापित करता है जो रिकर्सिव को-अल्जेब्रा के माध्यम से ग्लोबल ट्रेस कंडीशन (GTC) को अभिलक्षित करता है, जिससे अद्वितीय को-अल्जेब्रा-टू-अल्जेब्रा मोर्फिज्म के अस्तित्व के रूप में साउंडनेस का एक श्रेणीगत (categorical) सूत्रीकरण प्रदान किया जाता है।