1115 पेपर
यह शोध पत्र ZFLean को प्रस्तुत करता है, जो एक Lean 4 लाइब्रेरी है जो बेहतर एर्गोनॉमिक्स, कैनोनिकल कंस्ट्रक्शंस और सेट-लेवल एवं टाइप्ड प्रूफ के मिश्रण को सुगम बनाने के लिए नेटिव टाइप्स के साथ सेतु के रूप में, कोर ZFC सेट थ्योरी को Mathlib इकोसिस्टम के साथ एकीकृत करती है।
यह शोध पत्र हनोई ओमेगा-ऑटोमेटा (HOA) और नव-औपचारिक हनोई ओमेगा-गेम्स (HOG) की सैद्धांतिक जटिलता की पहली व्यवस्थित जांच प्रदान करता है, यह स्थापित करते हुए कि बूलियन ट्रांजिशन गार्ड्स के माध्यम से उनका प्रतीकात्मक एन्कोडिंग गैर-रिक्तता (non-emptiness) और भाषा समावेशन (language inclusion) जैसी मानक निर्णय समस्याओं को क्रमशः NP-पूर्ण और PSPACE/EXPSPACE-पूर्ण स्तरों तक बढ़ा देता है, जबकि विभिन्न स्वीकृति स्थितियों के तहत खेलों को हल करने के लिए सटीक जटिलता सीमाएं व्युत्पन्न करता है।
यह शोध पत्र वर्तमान स्वचालित प्रमाण संश्लेषण उपकरणों (automated proof synthesis tools) की सीमाओं का विश्लेषण करता है, यह पहचानता है कि सफलता के लिए मानव-समान टैक्टिक पैटर्न (human-like tactic patterns) अत्यंत महत्वपूर्ण हैं, और एक पैटर्न-गाइडेड टैक्टिक सर्च (PGTS) विधि प्रस्तावित करता है जो इंटरैक्टिव थ्योरम प्रूवर्स (interactive theorem provers) के लिए प्रमाण दरों और स्क्रिप्ट संक्षिप्तता में महत्वपूर्ण सुधार करता है।
यह शोध पत्र यह स्थापित करता है कि रिकरेंट न्यूरल नेटवर्क, पॉलिनोमियल ओडीई (ODE), और पॉलिनोमियल मैप्स, प्रिमिटिव रिकर्सिव फंक्शन्स की गणना करने के लिए समान रूप से तुल्य ढाँचे हैं, जो यह प्रकट करते हैं कि कैसे प्रत्येक प्रणाली अपने विशिष्ट गतिशील गुणों के माध्यम से एक-दूसरे की संरचनात्मक सीमाओं—जैसे कि ब्रांचिंग, राउंडिंग, या डिसक्रेटाइजेशन—की भरपाई करती है।
यह शोध पत्र CEGIW प्रस्तुत करता है, जो एक काउंटरएग्जांपल-गाइडेड एल्गोरिदम है जो प्रदर्शन में गिरावट का अनुभव करने वाले सिस्टम के लिए उनकी वैधता बहाल करने हेतु उनके मूल तार्किक संरचना को संरक्षित करते हुए मेट्रिक टेम्पोरल लॉजिक विनिर्देशों में टाइमिंग अंतराल को स्वचालित रूप से और इष्टतम रूप से कमजोर करता है।
यह शोध पत्र **NeSyCat** का प्रस्ताव करता है, जो एक श्रेणीबद्ध ढांचा (categorical framework) है जो ULLER न्यूरोसिम्बोलिक भाषा के विजातीय शास्त्रीय, फजी और संभाव्य अर्थों (semantics) को एक एकल मॉड्यूलर प्रणाली में एकीकृत करने के लिए मोनाड्स (monads) का उपयोग करता है, जो विभिन्न अर्थ संबंधी मॉडलों के बीच आसान विस्तार और अनुवाद की अनुमति देता है।
यह शोध पत्र IBV को प्रस्तुत करता है, जो BV तर्क का एक अंतर्ज्ञानवादी (intuitionistic) संस्करण है, जो कट उन्मूलन (cut elimination) के साथ एक गहन अनुमान प्रणाली (deep inference proof system) प्रदान करता है और यह प्रदर्शित करता है कि इसका गैर-साहचर्य (non-associative) संस्करण NML तर्क के एक नए अंतर्ज्ञानवादी संस्करण (INML) का निर्माण करता है जिसमें एक कट-मुक्त अनुक्रम गणक (cut-free sequent calculus) है।
यह शोधपत्र अनंतवत (infinitary) वस्तुओं के सह-आगमनात्मक (coinductive) पुनर्लेखन (rewriting) के लिए एक सामान्य ढांचे को प्रस्तुत करता है और "संपीड़न" (compression)—ट्रांसफाइनाइट पुनर्लेखन अनुक्रमों को लंबाई तक कम करने की क्षमता—को अभिलक्षणित करता है, तथा इस परिणाम को गैर-सुव्यवस्थित (non-wellfounded) प्रमाण प्रणाली में कट-उन्मूलन (cut-elimination) के संपीड़नीय होने को सिद्ध करने के लिए लागू करता है।
यह शोध पत्र GORED का प्रस्ताव करता है, जो एक सामान्य अनुकूलन सॉल्वर (optimization solver) है जो विविध अनुकूलन समस्याओं को स्वचालित रूप से MaxSAT उदाहरणों में कम करके समस्या-समाधान बहुमुखीता को बढ़ाता है, जिससे एक एकल एकीकृत ढांचा विशिष्ट एल्गोरिदम के तुलनीय समाधान गुणवत्ता प्राप्त करने में सक्षम होता है।
यह शोधपत्र "प्रायिकतात्मक अपोहन" (probabilistic abduction) की जटिलता को औपचारिक रूप देने और अध्ययन करने के लिए एक फजी प्रायिक तर्क () प्रस्तुत करता है, जो कि घटनाओं की प्रायिकता के बारे में दिए गए प्रेक्षणों से तार्किक रूप से निहित होने वाले प्रायिकता वितरणों या कथनों को खोजने की एक प्रक्रिया है।