1086 पेपर
यह शोधपत्र एक परिमित ऑडिट ढांचे को औपचारिक रूप देता है जो एक रिफाइनमेंट लैटिस के भीतर रिकॉर्ड डोमेन के उनके संबंधित विभाजनों की तुलना करके घोषित और कार्यान्वित पहचान नियमों के बीच व्यवस्थित विचलन का पता लगाता है, जिसमें अंतर्निहित कार्यान्वयन आधार को प्रकट किए बिना विशिष्ट विचलन साक्ष्यों की पहचान करने के लिए एक त्रि-मूल्यवान, गैर-एकदिष्ट मूल्यांकन का उपयोग किया जाता है।
यह शोध पत्र एक विशिष्ट "एंटी-गोल" (anti-goal) ढांचे और एक "प्रिवेंट" (prevent) मानसिक क्रिया को पेश करके नॉन-एक्सिओमैटिक लॉजिक के भीतर बचाव (avoidance) के प्रतिनिधित्व में निहित अस्पष्टता को संबोधित करता है, जिससे उन विरोधाभासों को हल किया जा सके जहाँ किसी घटना से बचने को उसके निषेध (negation) को प्राप्त करने के साथ मिला दिया जाता है, और प्रणालियों को लक्ष्य प्राप्ति, निष्क्रिय बचाव, सक्रिय रोकथाम और निष्क्रियता के बीच स्पष्ट रूप से अंतर करने में सक्षम बनाया जा सके।
यह शोध पत्र सिग्नल टेम्पोरल लॉजिक (STL) के मौजूदा टैब्लो विधियों में एक साउंडनेस दोष की पहचान करता है, एक सुधारात्मक साउंड और कंप्लीट ट्री-शेप्ड टैब्लो प्रस्तावित करता है, और STLSat पेश करता है, जो एक ओपन-सोर्स रस्ट (Rust) टूल है जो इस सैद्धांतिक आधार के साथ-साथ FOL/SMT एनकोडिंग का लाभ उठाकर साइबर-फिजिकल सिस्टम्स में संतुष्टि (satisfiability) की जांच करने, विटनेस (witnesses) को संश्लेषित करने और असंगत विशिष्टताओं को डीबग करने को प्रभावी ढंग से संचालित करता है।
यह शोध पत्र इस बात की गणनात्मक जटिलता (computational complexity) की जांच करता है कि क्या प्रपोजिशनल एब्डक्शन (propositional abduction) में स्पष्टीकरणों का एक दिया गया सेट, एक सीमित सममित अंतर (bounded symmetric difference) के भीतर किसी अन्य स्पष्टीकरण का प्रतिनिधित्व कर सकता है, जो एक पूर्ण शास्त्रीय जटिलता वर्गीकरण और एक पैरामीटराइज्ड विश्लेषण प्रदान करता है जो कोडिंग थ्योरी में कवरिंग रेडियस समस्या (covering radius problem) के साथ एक नवीन संबंध को प्रकट करता है।
यह शोध पत्र एक नवीन मैट्रिक्स-आधारित विभेदनीय तर्क प्रोग्रामिंग ढांचे (differentiable logic programming framework) का प्रस्ताव करता है जो नियमों और बाधाओं के एक एकीकृत एन्कोडिंग को नियोजित करके न्यूरोसिम्बोलिक प्रणालियों में रीजनिंग शॉर्टकट्स को कम करता है, और प्रयोगों के माध्यम से यह प्रदर्शित करता है कि न्यूरल आउटपुट का तार्किक परमाणुओं (logical atoms) के साथ एक-से-एक ग्राउंडिंग, बाधा संतुष्टि और संज्ञानात्मक शॉर्टकट्स को रोकने में पारंपरिक सॉफ्ट प्रोबेबिलिटी दृष्टिकोणों की तुलना में काफी बेहतर प्रदर्शन करता है।
यह शोध पत्र एक केस स्टडी प्रस्तुत करता है जो यह प्रदर्शित करता है कि कैसे एक LLM, बुनियादी लॉजिक प्रोग्रामिंग परिभाषाओं द्वारा निर्देशित और LPTP थ्योरम प्रूवर द्वारा सत्यापित, सफलतापूर्वक वर्गमूल 2 की अपरिमेयता का एक पूर्ण, मानव-पठनीय औपचारिक प्रमाण उत्पन्न कर सकता है।
यह शोधपत्र ग्रासरूट्स लॉजिक प्रोग्राम्स (GLP) को प्रस्तुत करता है, जो एक मल्टीएजेंट कंकरेंट लॉजिक प्रोग्रामिंग भाषा है जिसे ग्रासरूट्स प्लेटफॉर्म को लागू करने के लिए डिज़ाइन किया गया है जो स्वतंत्र संस्थाओं को स्वायत्त रूप से संचालित होने और केंद्रीकृत या प्लूटोक्रेटिक वैश्विक संसाधनों पर निर्भर हुए बिना बड़ी प्रणालियों में विलीन होने में सक्षम बनाती हैं।
यह शोध पत्र एक इंटरैक्टिव सीक्वेंट प्रूवर (sequent prover) प्रस्तुत करता है जो इवेंट-बी (Event-B) के लिए प्रोलॉग (Prolog) में कार्यान्वित है और प्रोब (ProB) टूल में एकीकृत है, जो पिछले जावा (Java) कार्यान्वयन की तुलना में एक अधिक संक्षिप्त और रखरखाव योग्य विकल्प प्रदान करता है और साथ ही प्रूफ़ ट्री विज़ुअलाइज़ेशन, रोडिन (Rodin) इंटरऑपरेबिलिटी, और प्रमाण निर्माण पर छात्रों के प्रत्यक्ष नियंत्रण के माध्यम से उन्नत शैक्षिक मूल्य सक्षम करता है।
यह शोध पत्र ProB के प्रोलॉग (Prolog) एनिमेशन मोड के हालिया विस्तार प्रस्तुत करता है, जिसमें उन्नत सिमुलेशन, ट्रेस रिप्ले, उपयोगकर्ता इनपुट और विज़ुअलाइज़ेशन सुविधाएँ शामिल हैं, जिन्हें रणनीति मूल्यांकन, इवेंट-बी (Event-B) प्रमाण सत्यापन और शैक्षिक प्रदर्शनों का समर्थन करने के लिए 'कनेक्ट फोर' (Connect Four) जैसे केस स्टडीज पर लागू किया गया है।
यह शोध पत्र LogMorph प्रस्तुत करता है, जो प्रोलॉग (Prolog) के लिए एक डेटा-संचालित उत्परिवर्तन ढांचा (mutation framework) है, जो वास्तविक क्लासरूम की गलतियों से मेल खाने वाले त्रुटि वितरण के साथ यथार्थवादी कृत्रिम दोष उत्पन्न करने के लिए 7,201 छात्र सबमिशन के एक अनुभवजन्य वर्गीकरण (empirical taxonomy) का लाभ उठाता है, जिससे लॉजिक प्रोग्रामिंग शिक्षा में स्वचालित फीडबैक टूल की प्रभावशीलता में सुधार होता है।