💻 Category

cs.LO

1115 पेपर

💻 computer science

Towards the Usage of Window Counting Constraints in the Synthesis of Reactive Systems to Reduce State Space Explosion

यह शोधपत्र एक पुनरावृत्ति संश्लेषण दृष्टिकोण (iterative synthesis approach) प्रस्तावित करता है जो विनिर्देश एकरूपता (specification monotonicity) का लाभ उठाने के लिए विंडो काउंटिंग बाधाओं (window counting constraints) का उपयोग करता है, जिससे रिएक्टिव सिस्टम रणनीतियों के स्वचालित निर्माण में स्टेट स्पेस विस्फोट (state space explosion) को काफी कम करने के लिए ओवर- या अंडर-एप्रोक्सिमेशन के साथ ऑटोमेटा का निर्माण किया जा सके।

Linda Feeken, Martin Fränzle2026-04-01
💻 computer science

Breaking Symmetries with Involutions

यह शोध पत्र इनवोल्यूशन परम्यूटेशन (involution permutations) से प्राप्त ग्राफ पैटर्न का लाभ उठाकर ग्राफों के लिए कुशल और शक्तिशाली सिमिट्री-ब्रेकिंग बाधाओं (symmetry-breaking constraints) के निर्माण हेतु एक नवीन दृष्टिकोण प्रस्तावित करता है, जो प्रभावी रूप से गैर-कैनोनिकल ग्राफों के एक महत्वपूर्ण हिस्से की पहचान करता है और उन्हें बाहर करता है, जबकि एक छोटे बाधा आकार को बनाए रखता है।

Michael Codish, Mikoláš Janota2026-04-01
🤖 AI

Generative Logic: A New Computer Architecture for Deterministic Reasoning and Knowledge Generation

यह शोध पत्र जेनेरेटिव लॉजिक (GL) को प्रस्तुत करता है, जो एक नियतात्मक (deterministic) कंप्यूटर आर्किटेक्चर है जो स्वयंसिद्ध परिभाषाओं को लॉजिक ब्लॉक्स के एक वितरित ग्रिड में संकलित करता है ताकि व्यवस्थित रूप से ऑडिट करने योग्य, पूर्ण-स्रोत (full-provenance) प्रमाण और संख्यात्मक गणनाएँ उत्पन्न की जा सकें, और सामान्य हार्डवेयर पर गौस के योग सूत्र जैसे जटिल गणितीय परिणामों को सफलतापूर्वक व्युत्पन्न कर सके।

Nikolai Sergeev2026-04-01
🔢 mathematics

Additive systems for Z\mathbb{Z} are undecidable

यह शोध पत्र यह प्रदर्शित करता है कि Z\mathbb{Z} के उपसमुच्चयों के एक मानक संग्रह के योगसमूह (sumset) द्वारा संपूर्ण पूर्णांकों को कवर करने का निर्धारण करना अनिर्णायक (undecidable) है, क्योंकि इस समस्या को फ्रैक्ट्रान (Fractran) के सार्वभौमिक रुकने की समस्या (universal halting problem) के समकक्ष दिखाया गया है और यह कोलात्ज़ अनुमान (Collatz conjecture) से जुड़ा हुआ है।

Andrei Zabolotskii2026-04-01
💻 computer science

Access Hoare Logic

यह शोध पत्र एक्सेस होअर लॉजिक (Access Hoare Logic) को प्रस्तुत करता है, जो कंप्यूटर प्रोग्रामों में एक्सेस कंट्रोल और सुरक्षा के बारे में तर्क करने के लिए एक नवीन औपचारिकता है, और इसकी सुदृढ़ता (soundness), पूर्णता (completeness), तथा मानक होअर लॉजिक और इनकरेक्टनेस लॉजिक दोनों से इसके मौलिक अंतरों को स्थापित करता है।

Arnold Beckmann, Anton Setzer2026-04-01
💻 computer science

From categorized neural architectures to subexponential proof theory

यह शोध पत्र एक वर्गीकृत, संसाधन-संवेदनशील तंत्रिका संरचना (neural architecture) से सीधे कट विलोपन (cut elimination) के साथ एक उप-चरघातांकीय (subexponential) प्रमाण प्रणाली प्राप्त करने के लिए एक ढांचा स्थापित करता है, यह प्रदर्शित करते हुए कि परिणामी तार्किक अनुशासन वास्तुशिल्प बाधाओं के प्रति सुसंगत है और वह वास्तुकला स्वयं एक सममित मोनॉइडल श्रेणी (symmetric monoidal category) बनाती है।

Carlos Ramírez Ovalle2026-04-01
💻 computer science

Near-Optimal Encodings of Cardinality Constraints

यह शोध पत्र कार्डिनैलिटी बाधाओं (cardinality constraints) के लिए नवीन, निकट-इष्टतम (near-optimal) CNF एनकोडिंग प्रस्तुत करता है जो पिछले तरीकों की तुलना में क्लॉज गणनाओं को काफी कम कर देता है, जिसमें AtMostOne के लिए एक नया एनकोडिंग शामिल है जो एक लंबे समय से चले आ रहे अनुमान का खंडन करता है, समस्या के लिए पहला गैर-तुच्छ बिना शर्त निचला स्तर (unconditional lower bound) स्थापित करता है, और एक 50 साल पुराने सर्किट जटिलता परिणाम में सुधार करता है, जबकि सामान्य AtMostk_k बाधाओं के लिए संक्षिप्त एनकोडिंग प्राप्त करने हेतु एक "ग्रिड कम्प्रेशन" तकनीक भी प्रस्तावित करता है।

Andrew Krapivin, Benjamin Przybocki, Bernardo Subercaseaux2026-04-01
💻 computer science

Loop-Checking and Counter-Model Extraction for Intuitionistic Tense Logics via Nested Sequents

यह शोध पत्र सहज बोधगम्य टेन्स लॉजिक (intuitionistic tense logics) के लिए एक नवीन नेस्टेड सीक्वेंटल प्रूफ-सर्च पद्धति प्रस्तुत करता है जो कंप्यूटेशन ट्री के निर्माण के लिए होमोमोर्फिज्म-आधारित लूप-चेकिंग का उपयोग करता है, जिससे परिमित काउंटर-मॉडेल्स को निकालना संभव होता है और विशिष्ट लॉजिक एक्सटेंशन के लिए फाइनाइट मॉडल प्रॉपर्टी (finite model property) को स्थापित किया जाता है।

Tim S. Lyon2026-04-01
💻 computer science

Compositional Reasoning for Probabilistic Automata with Uncertainty

यह शोधपत्र विविध प्रमेय नियमों (proof rules), एकतलता विश्लेषण (monotonicity analysis) और सिमुलेशन संबंधों के माध्यम से पैरामीट्रिक मॉडलों और रोबस्ट अंतराल-आधारित मॉडलों, दोनों को कवर करते हुए, अनिश्चित संक्रमण संभावनाओं वाले संभाव्य ऑटोमेटा (probabilistic automata) के संरचनात्मक सत्यापन (compositional verification) के लिए एक व्यापक 'असम-गारंटी' (assume-guarantee) ढांचे को स्थापित करता है।

Hannah Mertens, Tim Quatmann, Joost-Pieter Katoen2026-04-01
💻 computer science

A Graded Modal Dependent Type Theory with Erasure, Formalized

यह शोध पत्र Agda में एक पूर्णतः औपचारिक रूप से परिभाषित ग्रेडेड मोडल डिपेंडेंट टाइप थ्योरी प्रस्तुत करता है जो ग्रेड-आधारित वेरिएबल ट्रैकिंग के माध्यम से इरेज़र (erasure) जैसी गुणों को लागू करता है, और नॉर्मलाइज़ेशन, डैसिडेबिलिटी (decidability), तथा एक एक्सट्रैक्शन फंक्शन की सुसंगतता (soundness) सहित प्रमुख मेटा-थ्योरिटिक परिणामों को स्थापित करता है जो प्रोग्राम वैल्यूज को सुरक्षित रखते हुए इरेसेबल कंटेंट को हटा देता है।

Andreas Abel, Nils Anders Danielsson, Oskar Eriksson2026-04-01