cs.LO पेपर | Gist.Science

The Guarded Fragment with Nested Equivalences

यह शोध पत्र यह स्थापित करता है कि नेस्टेड इक्विवेलेंस रिलेशंस (nested equivalence relations) के साथ विस्तारित गार्डेड फ्रैगमेंट (Guarded Fragment) 'फाइनाइट मॉडल प्रॉपर्टी' (finite model property) को बनाए रखता है और TOWER-कम्प्लीट जटिलता (या संबंधों की एक निश्चित संख्या के लिए $(K{+}2)$ -ExpTime-कम्प्लीट) के साथ निर्णय योग्य (decidable) है, जबकि यह भी दर्शाता है कि नेस्टिंग की स्थिति को शिथिल करने या समानता (equality) को स्वीकार करने से संतुष्टि समस्या (satisfiability problem) अनिर्णायक (undecidable) हो जाती है।

Oskar Fiuk2026-05-15

💻 computer science

Loop Termination and Generalized Collatz Sequences

यह शोध पत्र पूर्णांकों पर एक-चर रैखिक-प्रतिबंध लूप (one-variable linear-constraint loops) की समाप्ति और सामान्यीकृत कोलात्ज़ अनुक्रमों (generalized Collatz sequences) के बीच एक घनिष्ठ संबंध स्थापित करता है, जो यह सिद्ध करता है कि इन अनुक्रमों के बारे में एक विशिष्ट अनुमान पर निर्भर करते हुए लूप की समाप्ति बहुपद समय (polynomial time) में निर्णायक (decidable) है, और साथ ही यह भी प्रदर्शित करता है कि ऐसे लूपों के लिए कोई भी निर्णय प्रक्रिया (decision procedure) इस अनुमान के खुले मामलों को हल कर देगी।

Mishel Carelli2026-05-15

🔢 mathematics

Guises and Perspectives: An Intentional and Hyperintensional Sketch

यह शोधपत्र कास्टानेडा के आंतरिकतावादी (internalist) और लाइबनिजियन दर्शन में निहित 'गिसेस' (guises) का एक औपचारिक तर्क प्रस्तुत करता है, जो एक वाक्य-रचना (syntax), मॉडल सिद्धांत (model theory) और प्रमाण सिद्धांत (proof theory) स्थापित करता है जहाँ संबंधों को बाहरी कारण संबंधी कड़ियों के बजाय गुणों के बंडलों (property bundles) के भीतर एनकोडेड इरादतन दृष्टिकोणों (intentional perspectives) के रूप में माना जाता है, जिससे हाइपरइंटेंशनल (hyperintensional) घटनाओं को संबोधित किया जा सके और शास्त्रीय इरादतन (intensional) एवं परिस्थिति अर्थविज्ञान (situation semantics) का एक विशिष्ट विकल्प प्रदान किया जा सके।

Juan J. Colomina-Alminana2026-05-15

💻 computer science

Automating Bitvector and Finite Field Equivalence Proofs in Lean

यह शोध पत्र BitModEq को प्रस्तुत करता है, जो एक नवीन Lean टैक्टिक है जो रेंज लेम्मा (range lemmas) और केस एनालिसिस (case analysis) का उपयोग करके बिटवेक्टर्स (bitvectors) और परिमित क्षेत्रों (finite fields) के बीच समानता प्रमाणों को स्वचालित करता है, जो ज़ीरो-नॉलेज प्रूफ (Zero-Knowledge Proof) सर्किट एनकोडिंग को सत्यापित करने में अत्याधुनिक SMT सॉल्वर से बेहतर प्रदर्शन करता है।

Elizaveta Pertseva, Valentin Robert, Clark Barrett, James Parker2026-05-15

💻 computer science

Work-Efficient Query Evaluation in Constant Time with PRAMs

यह शोध पत्र अनुमानित प्रिफिक्स सम (approximate prefix sums) और कॉम्पैक्शन तकनीकों का लाभ उठाकर, हल्के डेटा धारणाओं के तहत अचक्रीय (acyclic), सेमीजॉइन (semijoin), और वर्स्ट-केस ऑप्टिमल जॉइन (worst-case optimal join) प्रश्नों के मूल्यांकन के लिए CRCW PRAMs पर दुर्बल कार्य-कुशल (weakly work-efficient) निरंतर-समय एल्गोरिदम प्रस्तुत करता है, जो $\mathcal{O}(T^{1+\varepsilon})$ के कार्य बाउंड्स प्राप्त करते हैं।

Jens Keppeler, Thomas Schwentick, Christopher Spinrath2026-05-14

💻 computer science

Fully Evaluated Left-Sequential Logics

यह शोधपत्र 'फ्री' (Free) से लेकर 'स्टैटिक एफईएल' (Static FEL) तक के पूर्णतः मूल्यांकित बाएँ-क्रमिक तर्कशास्त्र (left-sequential logics) के एक पदानुक्रम को प्रस्तुत करता है, जो मूल्यांकन वृक्षों (evaluation trees) को एक अर्थ संबंधी आधार के रूप में उपयोग करते हुए उनके द्वि-मान और त्रि-मान संस्करणों के लिए पूर्ण अभिलेखन (axiomatisations) प्रदान करता है।

Alban Ponse, Daan J. C. Staudt2026-05-14

💻 computer science

Fracterm Calculus for Partial Meadows

यह शोधपत्र आंशिक मीडोज़ (partial meadows) के लिए तीन-मूल्यीय शॉर्ट-सर्किट लॉजिक (three-valued short-circuit logic) का उपयोग करते हुए एक फ्रैक्टर्म कैलकुलस (fracterm calculus) प्रस्तुत करता है ताकि विभाजन वाले क्षेत्रों (fields with division) का एक स्वाभाविक औपचारिकीकरण प्रदान किया जा सके, यह प्रदर्शित करते हुए कि यद्यपि यह तर्क शून्य द्वारा विभाजन की अनिर्धारित प्रकृति को व्यक्त नहीं कर सकता है, फिर भी इसका परिणाम संबंध (consequence relation) अर्ध-संगणनीय (semi-computable) है और इसके $\bot$ -विस्तार (enlargements) सामान्य मीडोज़ (common meadows) उत्पन्न करते हैं।

Jan A. Bergstra, Alban Ponse2026-05-14

💻 computer science

Dicey Games: Shared Sources of Randomness in Distributed Systems

यह शोधपत्र "डाइसी गेम्स" (Dicey Games) को प्रस्तुत करता है, जो साझा यादृच्छिकता (randomness) के स्रोतों वाले वितरित प्रणालियों के विश्लेषण के लिए एक औपचारिक ढांचा है, यह प्रदर्शित करते हुए कि टीमें युग्मवार साझा यादृच्छिकता को रणनीतिक रूप से आवंटित करके स्वतंत्र यादृच्छिकीकरण से अधिक की इष्टतम जीतने की संभावनाएँ प्राप्त कर सकती हैं और ऐसी रणनीतियों के अस्तित्व, प्रतिनिधित्व और कम्प्यूटेशनल जटिलता को अभिलक्षित करती है।

Léonard Brice, Thomas A. Henzinger, K. S. Thejaswini2026-05-14

💻 computer science

Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property

यह शोध पत्र प्रतीकात्मक संरचनाओं को मनमाने आधार सिद्धांतों (arbitrary base theories) तक सामान्यीकृत करता है और परिणामी प्रतीकात्मक मॉडल गुण का लाभ उठाकर उन कई प्रथम-क्रम तर्क खंडों (first-order logic fragments) की निर्णयक्षमता (decidability) को सिद्ध करता है जो विशिष्ट प्रतिबंधों के तहत स्व-लूपिंग फलनों (self-looping functions) की अनुमति देकर स्तरीकृत सूत्रों (stratified formulas) का विस्तार करते हैं।

Neta Elad, Sharon Shoham2026-05-14

💻 computer science

Formal Verification of Imperative First-Class Functions in Move

यह शोध पत्र मूव प्रोवर (Move Prover) का एक विस्तार प्रस्तुत करता है जो व्यवहारिक विधेयकों (behavioral predicates), अवस्था लेबल (state labels) और एक एसएमटी एनकोडिंग रणनीति (SMT encoding strategy) को पेश करके मूव भाषा में इम्पैरेटिव फर्स्ट-क्लास फंक्शन्स के औपचारिक सत्यापन को सक्षम बनाता है, जो कुशल सत्यापन और स्वचालित विनिर्देश अनुमान (automated specification inference) के लिए मूव के स्टैटिक मेमोरी सेपरेशन का लाभ उठाता है।

Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap, Jake Silverman2026-05-14

← पिछला अगला →