💻 Category

cs.LO

1086 पेपर

💻 computer science

Approximation theory for distant Bang calculus

यह शोध पत्र इस ढांचे के भीतर बोम ट्रीज़ (Böhm trees) और टेलर एक्सपेंशन (Taylor expansion) को परिभाषित करके, कॉल-बाय-नेम (Call-by-Name) और कॉल-बाय-वैल्यू (Call-by-Value) λ-कैलकुली के अलग-अलग सन्निकटन सिद्धांतों का सामान्यीकरण और समावेशन करते हुए, स्पष्ट प्रतिस्थापन (explicit substitutions) और दूरस्थ न्यूनीकरण (distant reductions) वाले बैंग-कैलकुलस (Bang-calculus) के लिए एक एकीकृत सन्निकटन अर्थविज्ञान (approximation semantics) विकसित करता है।

Kostia Chardonnet, Jules Chouquet, Axel Kerinec2026-07-01
🤖 machine learning

Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4

यह शोधपत्र नाज़्रिन (Nazrin) को प्रस्तुत करता है, जो लीन 4 (Lean 4) के लिए एक ग्राफ न्यूरल नेटवर्क-आधारित प्रमेय सिद्ध करने वाला एजेंट है, जो मजबूत, उपभोक्ता-ग्रेड हार्डवेयर-अनुकूल प्रमाण स्वचालन को सक्षम करने के लिए परमाणु युक्तियों (atomic tactics) के एक नवीन सेट, एक ट्रांसपोज़िंग एटमाइज़ेशन एल्गोरिदम और एक्सप्र ग्राफ (ExprGraph) डेटा संरचना का उपयोग करता है।

Leni Aniva, Iori Oikawa, David Dill, Clark Barrett2026-07-01
🔢 mathematics

On the Expressive Power of Inquisitive Team Logic and Inquisitive First-Order Logic

यह शोधपत्र यह प्रदर्शित करता है कि जबकि जिज्ञासु टीम तर्क (inquisitive team logic) वाक्यों के लिए प्रथम-क्रम तर्क (first-order logic) के अभिव्यंजक रूप से समतुल्य है, इसके खुले सूत्रों (open formulas) में स्पष्ट रूप से अधिक अभिव्यंजक शक्ति है, एक ऐसा परिणाम जो मानक जिज्ञासु प्रथम-क्रम तर्क तक विस्तृत होता है यह दिखाते हुए कि यह गैर-प्रथम-क्रम गुणों को व्यक्त कर सकता है और, एक रेंज-जनरेटिंग क्वांटिफायर (range-generating quantifier) के साथ संवर्धित होने पर, परिमितता (finiteness) को परिभाषित कर सकता है।

Juha Kontinen (University of Helsinki), Ivano Ciardelli (University of Padua)2026-07-01
💻 computer science

From Herbrand schemes to functional interpretation

यह शोध पत्र हर्ब्रैंड स्कीम्स (Herbrand schemes) के मूल अवधारणाओं को शास्त्रीय अनुक्रम गणन (classical sequent calculus) के एक कार्यात्मक व्याख्या के रूप में पुनर्गठित करता है, जो हर्ब्रैंड के प्रमेय (Herbrand's theorem) के विश्लेषण के लिए खेल-सिद्धांत संबंधी दृष्टिकोणों के साथ संरेखित एक स्वाभाविक कम्प्यूटेशनल परिप्रेक्ष्य प्रदान करता है।

Sebastian Enqvist-Pyk2026-07-01
🔢 mathematics

Relational Semantics for Flat Heyting-Lewis Logic

यह शोध पत्र "फ्लैट हेयटिंग-लुईस लॉजिक" (HLC-flat) के लिए संबंधात्मक अर्थविज्ञान प्रस्तुत करता है, जो कि एक सहज बोधगम्य तर्क (intuitionistic logic) का रूपांतर है जिसे एक सख्त निहितार्थ मोडैलिटी (strict implication modality) के साथ विस्तारित किया गया है जो अपने पहले तर्क में 'मीट्स' (meets) को संरक्षित करता है, और इसके पूर्णता गुण (completeness) तथा परिमित मॉडल गुण (finite model property) के साथ-साथ कई अभिधारणा विस्तारों (axiom extensions) के गुणों को स्थापित करता है।

Jim de Groot, Tadeusz Litak2026-07-01
💻 computer science

Automated Reasoning with Nested Datatypes

यह शोधपत्र नेस्टेड डेटाटाइप्स (nested datatypes) के एक सिद्धांत को प्रस्तुत करता है जो गैर-मानक मॉडलों (non-standard models) को रोकने के लिए डेटाटाइप्स और ऐरे (arrays) के संयोजन को प्रतिबंधित करता है, इसके लिए एक सिद्ध सही निर्णय प्रक्रिया (decision procedure) प्रदान करता है, और वास्तविक और निर्मित बेंचमार्क पर इस प्रक्रिया के एक कार्यान्वयन का मूल्यांकन करता है।

Tomer Hakak, Yoni Zohar, Andrew Reynolds, Clark Barrett, Cesare Tinelli2026-07-01
🤖 AI

HyPOLE: Hyperproperty-Guided Multi-Agent Reinforcement Learning under Partial Observation

यह शोध पत्र HyPOLE पेश करता है, जो एक नवीन ढांचा है जो आंशिक अवलोकन (partial observability) के तहत मल्टी-एजेंट सुदृढीकरण शिक्षण (Multi-Agent Reinforcement Learning) को निर्देशित करने के लिए HyperLTL-आधारित हाइपरप्रॉपर्टीज का लाभ उठाता है, और केंद्रीकृत प्रशिक्षण एवं विकेंद्रीकृत निष्पादन के एकीकरण के माध्यम से मानक बेंचमार्क पर बेसलाइन्स की तुलना में बेहतर प्रदर्शन प्रदर्शित करता है।

Arshia Rafieioskouei, Tzu-Han Hsu, Matthew Lucas, Borzoo Bonakdarpour2026-07-01
🤖 AI

Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

यह शोध पत्र यह तर्क देता है कि प्राकृतिक-भाषा-से-लीन (natural-language-to-Lean) औपचारिकीकरण का मूल्यांकन करने के लिए केवल लीन संकलन दरों (Lean compilation rates) पर निर्भर रहना भ्रामक है क्योंकि सिंटैक्टिक वैधता और सिमेंटिक निष्ठा के बीच एक महत्वपूर्ण अंतर है, और यह एक कठोर मानव-कैलिब्रेटेड सर्वसम्मति मीट्रिक का प्रस्ताव करता है तथा औपचारिक कथन की सटीकता में सुधार के लिए एलैबोरेशन फीडबैक (elaboration feedback) को सबसे महत्वपूर्ण हस्तक्षेप के रूप में पहचानता है।

Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy, Yi Xie, Zhi Wang, Maziar Raissi2026-07-01
🤖 AI

Beyond But-for Test: Counterfactual Explanation in Abstract Argumentation via Actual Causality (Extended Version)

यह शोधपत्र अमूर्त तर्कसंगतता (abstract argumentation) के लिए एक हस्तक्षेप-आधारित प्रतितथ्यात्मक तर्क (counterfactual reasoning) ढांचे को प्रस्तुत करता है जो तर्क की स्वीकृति को समीकरणों के रूप में कूटबद्ध करके और प्रीएम्प्शन (preemption) एवं ओवरडिटरमिनेशन (overdetermination) जैसी जटिल स्थितियों में सटीक कारणों की पहचान करने के लिए हालपर्न-पर्ल कार्य-कारणता (Halpern-Pearl causality) को लागू करके पारंपरिक 'बट-फॉर' (but-for) परीक्षण की सीमाओं को दूर करता है।

Siyi Liu, Muyun Shao, Beishui Liao2026-07-01
💻 computer science

Spatial Model Checking of Images via Minimised Models and Branching Bisimilarity

यह शोध पत्र अर्ध-विविक्त क्लोजर मॉडलों (quasi-discrete closure models) के स्थानिक मॉडल चेकिंग के लिए एक कुशल न्यूनीकरण विधि का प्रस्ताव और सत्यापन करता है, जो कोपा (CoPa) तुल्यता वर्गों की गणना करने हेतु उन्हें लेबल वाले ट्रांज़िशन सिस्टम के रूप में एनकोड करता है, और प्रोटोटाइप टूलचेन VoxMinX के माध्यम से महत्वपूर्ण प्रदर्शन सुधारों को प्रदर्शित करता है।

Vincenzo Ciancia, Jan Friso Groote, Diego Latella, Mieke Massink, Erik P. de Vink2026-07-01