cs.LO पेपर | Gist.Science

Model checking with temporal graphs and their derivative

यह शोध पत्र टेम्पोरल ग्राफ्स के लिए कुरसेल के प्रमेय (Courcelle's Theorem) का पहला अनुकूलन प्रस्तावित करता है जो लाइफटाइम पर स्पष्ट निर्भरता से बचता है, ट्री-विड्थ (tree-width) और ट्विन-विड्थ (twin-width) को परिभाषित करने के लिए एक स्लाइडिंग टाइम विंडो पर अवकलज (derivative) की अवधारणा पेश करता है, और एक टेम्पोरल लॉजिक के लिए मेटा-थ्योरम स्थापित करता है जो टेम्पोरल क्लिक्स (temporal cliques) जैसी विविध समस्याओं को हल करने में सक्षम है।

Binh-Minh Bui-Xuan, Florent Krasnopol, Bruno Monasson, Nathalie Sznajder2026-03-10

💻 computer science

Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications

यह शोध पत्र सिंटेक्स गाइडेड सिंथेसिस (Syntax Guided Synthesis) को टेम्पोरल स्ट्रीम लॉजिक (TSL $_f$ ) के एक परिमित-प्रिफिक्स व्याख्या (finite-prefix interpretation) के साथ जोड़कर निष्पादन ट्रेसेस (execution traces) से डेटा-जागरूक टेम्पोरल विनिर्देशों (data-aware temporal specifications) को खनन करने के लिए एक नवीन दृष्टिकोण प्रस्तावित करता है, जो डेटा रूपांतरणों और टेम्पोरल व्यवहारों दोनों को समाहित करने वाले रिएक्टिव प्रोग्रामों के सुदृढ़ और नमूना-कुशल संश्लेषण (sample-efficient synthesis) को सक्षम बनाता है।

Sam Nicholas Kouteili, William Fishell, Christian Scaff, Mark Santolucito, Ruzica Piskac2026-03-10

🔢 mathematics

Three Fixed-Dimension Satisfiability Semantics for Quantum Logic: Implications and an Explicit Separator

यह शोध पत्र क्वांटम तर्क के लिए तीन निश्चित-आयामी संतुष्टता अर्थशास्त्र (satisfiability semantics) — मानक हिल्बर्ट-लैटिस, वैश्विक कम्यूटिंग-प्रोजेक्टर, और स्थानीय आंशिक-बुलियन — की तुलना करता है, जो एक सख्त पदानुक्रम को सिद्ध करता है जहाँ मानक अर्थशास्त्र अन्य दोनों की तुलना में स्पष्ट रूप से अधिक अभिव्यंजक है, जैसा कि एक स्पष्ट सूत्र द्वारा प्रदर्शित किया गया है जो सभी आयामों $d \ge 2$ के लिए मानक अर्थशास्त्र में संतुष्ट है लेकिन अन्य दो के अंतर्गत असंतोषजनक है।

Joaquim Reizi Higuchi2026-03-10

💻 computer science

LLM2SMT: Building an SMT Solver with Zero Human-Written Code

यह शोध पत्र LLM2SMT प्रस्तुत करता है, जो एक केस स्टडी के रूप में यह प्रदर्शित करता है कि कैसे एक LLM कोडिंग एजेंट बिना किसी मानव-लिखित कोड के, Nieuwenhuis-Oliveras कॉंग्रुएंस क्लोजर एल्गोरिदम और Lean प्रूफ एमिशन सहित, QF_UF के लिए एक पूर्ण, प्रतिस्पर्धी DPLL(T)-शैली का SMT सॉल्वर स्वायत्त रूप से बना सकता है।

Mikoláš Janota, Mirek Olšák2026-03-10

💻 computer science

Learning to Rank the Initial Branching Order of SAT Solvers

यह शोध पत्र CDCL SAT सॉल्वर के लिए प्रारंभिक ब्रांचिंग क्रम (branching orders) की भविष्यवाणी करने हेतु ग्राफ न्यूरल नेटवर्क का उपयोग करने का प्रस्ताव देता है, जो रैंडम और स्यूडो-इंडस्ट्रियल बेंचमार्क पर महत्वपूर्ण गति वृद्धि प्रदर्शित करता है, साथ ही यह भी उल्लेख करता है कि यह दृष्टिकोण जटिल इंडस्ट्रियल इंस्टेंस के मामले में संघर्ष करता है क्योंकि सॉल्वर के डायनेमिक ह्यूरिस्टिक्स भविष्यवाणियों को ओवरराइड कर देते हैं।

Arvid Eriksson (KTH Royal Institute of Technology), Gabriel Poesia (Kempner Institute at Harvard University), Roman Bres (…)2026-03-10

💻 computer science

Sketch-Oriented Databases

यह शोध पत्र स्केच-ओरिएंटेड डेटाबेस पेश करता है, जो एक श्रेणीगत ढांचा (categorical framework) है जो परिमित-सीमा स्केच (finite-limit sketches) के माध्यम से विभिन्न ग्राफ-आधारित प्रतिमानों और विशेषताओं को एकीकृत करता है, साथ ही लेज़ी पाथ इन्फरेंस (lazy path inference) के लिए लोकलाइज़र और मॉड्यूलर कंपोजिशन एवं स्केलेबल मॉडल विकास को सक्षम करने के लिए स्टटरिंग स्केच (stuttering sketches) का प्रस्ताव देता है।

Dominique Duval, Rachid Echahed2026-03-10

🔢 mathematics

Proceedings Eighth International Conference on Applied Category Theory

यह शोध पत्र आठवें अंतर्राष्ट्रीय अनुप्रयुक्त श्रेणी सिद्धांत (ACT2025) के कार्यवाही विवरण को प्रस्तुत करता है, जो जून 2025 में फ्लोरिडा विश्वविद्यालय में आयोजित किया गया था, जिसमें कंप्यूटर विज्ञान, क्वांटम कंप्यूटेशन और रसायन विज्ञान जैसे शुद्ध और अनुप्रयुक्त विषयों के विविध योगदान शामिल थे।

Amar Hadzihasanovic (Tallinn University of Technology), Jean-Simon Pacaud Lemay (Macquarie University)2026-03-10

💻 computer science

Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar

यह शोध पत्र Apply2Isar का परिचय देता है, जो एक ऐसा टूल है जो स्वचालित रूप से Isabelle/HOL में प्रक्रियात्मक (procedural) apply-शैली के प्रमाणों को पठनीय और सुदृढ़ घोषणात्मक (declarative) Isar प्रमाणों में परिवर्तित करता है, और Isabelle Archive of Formal Proofs के एक बड़े बेंचमार्क सेट पर मूल्यांकन के माध्यम से इसकी प्रभावशीलता को प्रदर्शित करता है।

Sage Binder, Hanna Lachnitt, Katherine Kosaian2026-03-10

💻 computer science

The Unit Gap: How Sharing Works in Boolean Circuits

यह शोध पत्र यह स्थापित करता है कि AIG आधार पर इष्टतम बूलियन सर्किट और फॉर्मूला के बीच आकार का अंतर सख्ती से 0 या 1 तक सीमित है, जो उन सटीक स्थितियों को स्पष्ट करता है जिनके तहत शेयरिंग (sharing) होती है और यह सिद्ध करता है कि कोई भी गैर-शून्य अंतराल विशेष रूप से फैन-आउट 2 वाले एक एकल गेट से उत्पन्न होता है।

Kirill Krinkin2026-03-10

🔢 mathematics

Central Limits via Dilated Categories

यह शोध पत्र केंद्रीय सीमा प्रमेयों (सेंट्रल लिमिट थीम्स) के लिए एक एकीकृत ढांचे के रूप में डिलेटेड सेमीनॉर्म-एनरिच्ड कैटेगरी थ्योरी को प्रस्तुत करता है, जो एक अमूर्त सीएलटी (CLT) स्थापित करता है जो शास्त्रीय परिणामों को पुनः प्राप्त करता है और सिम्प्लेक्टिक मैनिफोल्ड्स एवं सांख्यिकीय यांत्रिकी में नवीन अनुप्रयोग प्रदान करता है।

Henning Basold, Oisín Flynn-Connolly, Chase Ford, Hao Wang2026-03-10

← पिछला अगला →