1117 पेपर
यह शोधपत्र न्यूरल एडिटिव मॉडल्स (NAMs) के लिए एक कुशल, मॉडल-विशिष्ट एल्गोरिदम प्रस्तुत करता है जो लॉगरिदमिक क्वेरी जटिलता के साथ प्रमाणित रूप से कार्डिनल-मिनिमल स्पष्टीकरण उत्पन्न करता है, जो मानक न्यूरल नेटवर्क की कम्प्यूटेशनल जटिलता को दूर करते हुए स्पष्टीकरण के आकार और गणना समय दोनों में मौजूदा विधियों से बेहतर प्रदर्शन करता है।
यह अध्याय सार्वभौमिक प्रमाण-सिद्धांत (universal proof theory) के ढांचे के भीतर शास्त्रीय, सहज बोधपरक (intuitionistic), मोडल और उप-संरचनात्मक (substructural) तर्कशास्त्रों में क्रेग और एकसमान अंतर्वेशन (uniform interpolation) गुणों को स्थापित करने के लिए रचनात्मक, वाक्य-संचालित (syntax-driven) प्रमाण-सैद्धांतिक विधियों, विशेष रूप से माएहारा (Maehara) और पिट्स (Pitts) की तकनीकों का एक व्यापक अवलोकन प्रस्तुत करता है।
यह शोध पत्र यूनिट इक्वेशनल फ्रैगमेंट (unit equational fragment) के लिए ऑटोमेटेड थ्योरम प्रूवर्स से सैचुरेटेड क्लॉज सेट्स (saturated clause sets) को स्पष्ट, सत्यापन योग्य अनंत काउंटर-मॉडेल्स (infinite countermodels) में रूपांतरित करने की एक विधि प्रस्तुत करता है, वैम्पायर (Vampire) और ई (E) प्रूवर्स में इस दृष्टिकोण को लागू करता है, और इक्वेशनल थ्योरीज प्रोजेक्ट (Equational Theories Project) पर इसकी प्रभावशीलता को प्रदर्शित करता है।
यह शोधपत्र सार्वभौमिक परिमाणकों (universal quantifiers) और अनइंटरप्रिटेड फंक्शन सिम्बल्स (uninterpreted function symbols) को संयोजित करने वाले सूत्रों के लिए एक इंडक्टिव सैटिस्फिएबिलिटी सर्टिफिकेशन पद्धति प्रस्तुत करता है, जो उन मामलों में सैटिस्फिएबिलिटी को सफलतापूर्वक सिद्ध करता है जहाँ वर्तमान SMT सॉल्वर स्पष्ट मॉडल बनाने में असमर्थता के कारण विफल हो जाते हैं।
यह शोध पत्र बर्नैज़-शौन्फेलकल वर्ग के एक PSPACE-पूर्ण उप-खंड को प्रस्तुत करता है जो क्वांटिफाइड बुलियन फॉर्मूला के दो-खिलाड़ी खेल अर्थ विज्ञान को संरक्षित करता है, जिससे विभिन्न स्तरों के बहुपद पदानुक्रम (पॉलीनोमियल हाइरार्की) में TPTP लाइब्रेरी समस्याओं का वर्गीकरण सक्षम होता है।
यह शोध पत्र ICaTT को प्रस्तुत करता है, जो CaTT टाइप थ्योरी का एक रूढ़िवादी विस्तार (conservative extension) है, जो तुल्यता (equivalences) और -इक्विफाइब्रेशन ( -equifibrations) के संक्षिप्त औपचारिकीकरण को सुगम बनाने के लिए कोइंडक्टिव इनवर्टिबिलिटी (coinductive invertibility) को सम्मिलित करता है, जिसे एक कार्यान्वयन और मार्क्ड वीक -कैटेगरी (marked weak -categories) में एक सिमेंटिक व्याख्या द्वारा समर्थित किया गया है।
यह शोध पत्र अनिश्चित नियमों और प्रमेयों वाले अमूर्त (abstract) और संरचित (structured) तर्क ढांचों की तुलना करने के लिए अभिव्यक्ति (expressivity) की एक एकीकृत अवधारणा प्रस्तुत करता है, जो दोनों सकारात्मक और नकारात्मक परिणाम प्रस्तुत करता है जो अपूर्ण अमूर्त ढांचों और ASPIC+ की सापेक्ष क्षमताओं को स्थापित करते हैं।
यह शोध पत्र लीन कंप्यूटर साइंस लाइब्रेरी (CSLib) के भीतर हेनेसी-मिलनर लॉजिक का एक सामान्य, पुन: प्रयोज्य औपचारिक रूप प्रस्तुत करता है, जिसमें एक पूर्ण मेटाथ्योरी शामिल है जो हेनेसी-मिलनर प्रमेय को समाहित करती है और स्वैच्छिक इमेज-फाइनाइट लेबल वाले ट्रांज़िशन सिस्टम्स (labelled transition systems) का समर्थन करने के लिए लीन के ऑटोमेशन का लाभ उठाती है।
यह शोध पत्र यह स्थापित करता है कि एक निश्चित टोपोलॉजिकल माइनर (topological minor) को वर्जित करने वाले ग्राफ वर्गों पर डिसजॉइंट-पाथ्स लॉजिक (+) के लिए मॉडल चेकिंग समस्या फिक्स्ड-पैरामीटर ट्रैक्टेबल (fixed-parameter tractable) है, जिससे अनिवार्य रूप से सबग्राफ-क्लोज्ड (subgraph-closed) वर्गों पर इस लॉजिक की ट्रैक्टेबिलिटी संबंधी प्रश्न का समाधान होता है।
यह शोध पत्र प्रस्तुत करता है, जो सामान्य पुनरावृत्ति (general recursion) वाला एक हाइब्रिड क्वांटम प्रोग्रामिंग भाषा है जो प्रोग्राम रनटाइम को क्वांटम सर्किट आकार से जोड़कर जेनेरिक रिसोर्स विश्लेषण की सुविधा प्रदान करता है, जिससे क्वांटम सर्किट जटिलता को सीमित करने के लिए शास्त्रीय टर्मिनेशन तकनीकों के अनुकूलन को सक्षम बनाया जा सके।