1117 पेपर
यह शोध पत्र DLp को प्रस्तुत करता है, जो एक नवीन, पैरामीट्रिक डायनेमिक लॉजिक फ्रेमवर्क है जो किसी प्रोग्राम के ऑपरेशनल सिमेंटिक्स पर सीधे आधारित मॉडल-स्वतंत्र इन्फरेंस नियमों को प्रदान करके प्रोग्राम वेरिफिकेशन को सरल बनाता है, जो चक्रीय तर्क (cyclic reasoning) और मौजूदा सिद्धांतों के साथ अनुकूलता दोनों का समर्थन करता है।
यह शोध पत्र क्लोन (clones) के लिए एक प्रोफ़ाइनाइट पूर्णता (profinite completion) का निर्माण करने हेतु कोडेन्सिटी मोनाड्स (codensity monads) की श्रेणीबद्ध अवधारणा (categorical notion) का उपयोग करके नियमित ट्री भाषाओं (regular tree languages) के लिए एक टोपोलॉजिकल दृष्टिकोण प्रस्तुत करता है, जो मोनोइड्स (monoids) की प्रोफ़ाइनाइट पूर्णता का सामान्यीकरण करता है और प्रोफ़ाइनाइट पेड़ों (profinite trees) को प्रोफ़ाइनाइट लैम्ब्डा-कैलकुलस (profinite lambda-calculus) के एक विशिष्ट खंड के रूप में पहचानता है।
यह शोध पत्र 1950 के दशक से दर्शनशास्त्र में क्रेग इंटरपोलेशन और बेथ डेफिनैबिलिटी प्रमेयों के अनुप्रयोगों का एक ऐतिहासिक अवलोकन प्रदान करता है, जिसमें "निर्भरता" को एक केंद्रीय विषय के रूप में पहचानते हुए तार्किक अनुवादों और सामान्यीकृत डेफिनैबिलिटी पर नए तकनीकी निष्कर्ष प्रस्तुत किए गए हैं।
यह शोध पत्र एक आधार बहुपद (base polynomial) और एक विशिष्ट क्रमपरिवर्तन समूह (permutation group) के आधार पर बहुपद समरूपता-भंग बाधाओं (polynomial symmetry-breaking constraints) के एक यादृच्छिक परिवार को स्वचालित रूप से उत्पन्न करने के लिए एक बीजगणितीय विधि प्रस्तावित करता है, जो बिन पैकिंग केस स्टडी के माध्यम से यह प्रदर्शित करता है कि सरल द्विघात बाधाएं (quadratic constraints) पूर्णांक प्रोग्रामिंग समाधान समय को कम करने में विशेष रूप से प्रभावी हैं।
यह शोध पत्र बैंडविड्थ कलरिंग समस्या के लिए छह SAT एनकोडिंग विधियों का एक व्यवस्थित अध्ययन और एकीकृत ढांचा प्रस्तुत करता है, जो यह प्रदर्शित करता है कि ब्लॉक एनकोडिंग को इंक्रीमेंटल सॉल्विंग और सिमेट्री ब्रेकिंग के साथ मिलाने से अत्याधुनिक प्रदर्शन प्राप्त होता है और पहले अगम्य रहे उदाहरणों को प्रमाणित इष्टतमता तक हल किया जा सकता है।
यह शोधपत्र एक लीनियर कॉम्बिनेटरी अल्जेब्रा का उपयोग करते हुए लीनियर डिपेंडेंट टाइप थ्योरी के लिए एक रियलाइज़ेबिलिटी मॉडल का औपचारिक निर्माण प्रस्तुत करता है, जिसमें एक इम्प्रेडिकेटिव यूनिवर्स और विशिष्ट नियम पेश किए गए हैं जो लीनियर इंडक्टिव टाइप्स को एनकोड करने में सक्षम बनाते हैं।
यह शोध पत्र अनटाइप्ड प्रूफ-स्ट्रक्चर्स (untyped proof-structures) पर एक ज्यामितीय स्थिति प्रस्तुत करता है जो एक ज्ञात आवश्यक कनेक्टिविटी गुण को लीनियर लॉजिक के विशिष्ट खंडों के लिए एक पर्याप्त शुद्धता मानदंड में परिवर्तित करता है, जिससे सिक्वेंट कैलकुलस प्रमाणों की रिकवरी और नियम क्रमपरिवर्तन (rule permutations) का अभिलक्षण संभव हो पाता है।
यह शोध पत्र पिछले पांच वर्षों में प्रेडिक्टिव मेंटेनेंस (पूर्वानुमानित रखरखाव) में विशुद्ध रूप से डेटा-संचालित और पारंपरिक ज्ञान-आधारित दृष्टिकोणों की सीमाओं की समीक्षा करता है, और अधिक सटीक, व्याख्या योग्य और सुदृढ़ औद्योगिक प्रणालियों के लिए डीप लर्निंग को सिम्बोलिक लॉजिक (प्रतीकात्मक तर्क) के साथ एकीकृत करने हेतु न्यूरो-सिम्बोलिक एआई को अपनाने का तर्क देता है।
यह शोध पत्र द्वितीय-क्रम के सहज बोधवादी काल तर्क (सेकंड-ऑर्डर इंट्यूशनिस्टिक टेंस लॉजिक) के स्वयंसिद्ध, प्रमाण-सिद्धांतिक और मॉडल-सिद्धांतिक परिभाषाओं की समतुल्यता स्थापित करता है, जो यह प्रदर्शित करता है कि डायमंड मोडैलिटी को द्वितीय-क्रम परिमापन (सेकंड-ऑर्डर क्वांटिफिकेशन) के माध्यम से बॉक्स से व्युत्पन्न किया जा सकता है और सहज बोधवादी एवं शास्त्रीय दोनों वेरिएंटों के लिए एक लेबल वाले अनुक्रम गणन पद्धति (लेबल युक्त सीक्वेंट कैलकुलस) की पूर्णता और कट-स्वीकार्यता को सिद्ध करता है।