cs.LO

Interpolation via Generalized Splitting

Convex Biproducts, Stochastic Matrices and Tape Diagrams

यह शोध पत्र एक स्टोकेस्टिक मैट्रिक्स-आधारित कैलकुलस और संभाव्य परिवेशों के लिए एक ग्राफिकल फ्रेमवर्क स्थापित करने हेतु उत्तल बाइप्रोडक्ट्स (convex biproducts) के साथ श्रेणियों को प्रस्तुत करता है, जो अंततः संभाव्य बूलियन सर्किट का एक पूर्ण स्वयंसिद्धीकरण (axiomatisation) प्रदान करता है।

Justification Logic of the Lambda Calculus

यह शोधपत्र एक औचित्य तर्क (justification logic) प्रस्तुत करता है जहाँ प्रमाण पदों (proof terms) को स्पष्ट रूप से टाइप किए गए $\lambda$-पदों के साथ पहचाना जाता है, जो कर्ली-हावर्ड पत्राचार (Curry-Howard correspondence) के तहत गणना और प्रमाण के बारे में तर्क को एकीकृत करने के लिए एक स्वयंसिद्धीकरण (axiomatization), प्राकृतिक निगमन प्रणाली (natural deduction system) और एक कट-उन्मूलन वाले अनुक्रम पंचांग (cut-eliminating sequent calculus) को प्रदान करता है।

Automating the Derivation of Unification Algorithms: A Case Study in Deductive Program Synthesis

यह शोध पत्र डिडक्टिव प्रोग्राम सिंथेसिस का उपयोग करके एक तीन-तर्क वाले यूनिफिकेशन एल्गोरिदम के पूर्णतः स्वचालित व्युत्पन्न को प्रस्तुत करता है, जो मैन्युअल रूप से मना और वाल्डिंगर द्वारा किए गए प्रमाण का सामान्यीकरण और स्वचालन करता है ताकि एक संचित वातावरण प्रतिस्थापन (accumulating environment substitution) के सापेक्ष सर्वाधिक-सामान्य इडेम्पोटेंट यूनिफायर (most-general idempotent unifiers) की गणना करने वाला एक सही प्रोग्राम उत्पन्न किया जा सके।

Termination Analysis of Linear-Constraint Programs

यह सर्वेक्षण रैखिक-प्रतिबंध कार्यक्रमों (linear-constraint programs) के समापन के विश्लेषण की तकनीकों की व्यवस्थित रूप से समीक्षा करता है, जिसमें मौलिक निर्णयक्षमता परिणामों (decidability results), रैंकिंग फलनों (ranking functions), और विविक्त सुदृढ़ संक्रमण अपरिवर्तों (disjunctive well-founded transition invariants) को शामिल करते हुए अभिव्यंजक शक्ति और गणनात्मक जटिलता के बीच के समझौतों का परीक्षण किया गया है, हालांकि यह वास्तविक दुनिया की भाषाओं और गैर-रैखिक अंकगणित या संभाव्य चयन जैसे अधिक जटिल मॉडलों को वर्जित करता है।

On the Depth Scalability of Logic Gate Networks

यह शोध पत्र इनपुट-एंकोर्ड लॉजिक गेट नेटवर्क्स (IALGNs) को प्रस्तुत करता है, जो एक नवीन आर्किटेक्चर है जो प्रत्येक परत को मूल इनपुट से जोड़कर पारंपरिक लॉजिक गेट नेटवर्क्स की गहराई स्केलेबिलिटी सीमाओं को दूर करता है, जिससे 100 परतों से अधिक के नेटवर्क्स में भी स्थिर अनुकूलन और निरंतर सटीकता सुधार सक्षम होता है।

Three-player Differential Game Logic

यह शोधपत्र dGL3 प्रस्तुत करता है, जो एक तीन-खिलाड़ी विभेदक गेम लॉजिक (differential game logic) है जिसमें एक सुदृढ़ और अपेक्षाकृत पूर्ण प्रमाण पंचांग (proof calculus) है, जिसे उन गैर-शून्य-योग हाइब्रिड खेलों को सत्यापित करने के लिए डिज़ाइन किया गया है जहाँ व्यक्तिगत लक्ष्यों वाले खिलाड़ी गठबंधन बना सकते हैं, जिससे साझा सुरक्षा उद्देश्यों वाले परिदृश्यों में शून्य-योग धारणाओं की अत्यधिक रूढ़िवादी सीमाओं को दूर किया जा सके।

Machine-Checked Arithmetic Bit Complexity of the Kannan-Bachem Smith Normal Form in Lean 4

यह शोधपत्र गैर-एकल (nonsingular) पूर्णांक आव्यूहों (integer matrices) के लिए कन्नन-बेशम स्मिथ सामान्य रूप (Kannan-Bachem Smith normal form) एल्गोरिदम का लीन 4 (Lean 4) में एक औपचारिकीकरण प्रस्तुत करता है, जो शुद्धता के मशीन-चेक किए गए प्रमाण प्रदान करता है और गणना की अंकगणितीय बिट जटिलता (arithmetic bit complexity) तथा इसके आउटपुट के आकार, दोनों के लिए निश्चित बहुपद सीमाएं (fixed polynomial bounds) स्थापित करता है।

$Δ$-Nets: Interaction-Based System for Optimal Parallel $λ$-Reduction

यह शोध पत्र $\Delta$-Nets को प्रस्तुत करता है, जो एक इंटरेक्शन-आधारित मॉडल है जो $\lambda$-टर्म्स को एक अधिक लचीली संरचना में अनुवादित करके इष्टतम समानांतर $\lambda$-रिडक्शन को सक्षम बनाता है, जिससे एक लंबे समय से चली आ रही कम्प्यूटेशनल चुनौती का समाधान होता है और अधिक कुशल समानांतर प्रोग्रामिंग भाषाओं और आर्किटेक्चर के लिए मार्ग प्रशस्त होता है।

Modeling Deontic Modal Logic in ASP

यह शोध पत्र दायित्वों (obligations), निषेधों (prohibitions) और अनुमतियों (permissions) को दर्शाने के लिए ग्लोबल कंस्ट्रेंट्स (global constraints) के साथ डिफ़ॉल्ट और स्ट्रॉन्ग नेगेशन (default and strong negation) का उपयोग करके, आंसर सेट प्रोग्रामिंग (ASP) में डियोन्टिक मोडल लॉजिक (deontic modal logic) को लागू करने की एक सुरुचिपूर्ण विधि प्रस्तावित करता है, जिससे लंबे समय से चले आ रहे विरोधाभासों को हल किया जा सके और सशर्त डियोन्टिक कथनों के मॉडलिंग को सक्षम बनाया जा सके।