💻 Category

cs.LO

1090 पेपर

💻 computer science

From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware

यह शोध पत्र Encore! प्रस्तुत करता है, जो एक बेयर-मेटल कंटिन्यूएशन पासिंग स्टाइल (Continuation Passing Style) वर्चुअल मशीन है, जो कोर को एक प्रुवेबल स्टेट-ट्रांजिशन फंक्शन के रूप में संरचित करके माइक्रोकंट्रोलर्स पर औपचारिक रूप से सत्यापित, रॉक (Rocq) द्वारा एक्सट्रैक्ट किए गए स्कीम (Scheme) फर्मवेयर के निष्पादन को सक्षम बनाता है, जिससे मशीन-चेक्ड गारंटी के साथ सुरक्षा-महत्वपूर्ण कोड के एआई-सहायता प्राप्त जनरेशन को सुगम बनाया जा सके।

Valentin Bergeron, Karolina Gorna2026-06-03
💻 computer science

Diamonds Are Forever: Stabilization Semantics for Unrestricted Aggregation and Recursion in Logica

यह शोधपत्र डिफेंडेंट-अपोनेंट (DO) सिमेंटिक्स प्रस्तुत करता है, जो एक स्थिरीकरण-आधारित ढांचा है जो गेम-थ्योरेटिक डिफेंस और मोडल लॉजिक के माध्यम से सत्य को अभिलक्षणिक बनाकर लॉजिका भाषा में अनियंत्रित एकत्रीकरण और पुनरावृत्ति की अर्थ संबंधी चुनौतियों का समाधान करता है, जिससे गैर-मोनोटोनिक प्रोग्रामों का कठोर मूल्यांकन सक्षम होता है जो पारंपरिक फिक्स्पॉइंट तक पहुंचे बिना अभिसरित होते हैं।

Evgeny Skvortsov, Yilin Xia, Ojaswa Garg, Shawn Bowers, Bertram Ludäscher2026-06-03
💬 NLP

ZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics

यह शोध पत्र ZX-कैलकुलस (ZX-Calculus) प्रस्तुत करता है, जो मार्टिन-लोफ़ डिपेंडेंट टाइप थ्योरी (Martin-Löf Dependent Type Theory) का एक रूढ़िवादी विस्तार है जो ट्रेस-इंडेक्स्ड प्रकारों (trace-indexed types), प्रेशेफ नॉन-मोनोटोनिक सिमेंटिक्स (presheaf non-monotone semantics) और रचनात्मक AGM विश्वास संशोधन (constructive AGM belief revision) को एकीकृत करता है, जो एक कोक-सत्यापित (Coq-verified) ढांचा प्रदान करता है जो प्रमुख प्रमेयों को स्थापित करता है और पाथ-डिपेंडेंट विश्वास संशोधन और फंक्टर निरंतरता (functor consistency) के बीच एक मौलिक तनाव को प्रकट करता है।

Peng Chen2026-06-03
🔢 mathematics

Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents

यह शोध पत्र लीनियर टेम्पोरल लॉजिक (LTL) के लिए नॉन-वेलफाउंडेड और साइक्लिक लीनियर नेस्टेड सिक्वेंट कैलकुली पेश करता है और अभिव्यंजक मल्टीसिक्वेंट फॉर्मलिज्म की चुनौतियों को संबोधित करने के लिए चक्र पहचान (cycle recognition) और अनरैवलिंग (unraveling) की विधियों को विकसित करके उनके बीच एक सिंटैक्टिक पत्राचार स्थापित करता है।

Tim S. Lyon, Lukas Zenger2026-06-03
🔢 mathematics

Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents

यह शोध पत्र ट्री-हाइपरसीक्वेंट्स (tree-hypersequents) पर एक "रैखिकीकरण विधि" (linearization method) का उपयोग करके गोडेल-लोब लॉजिक (Gödel-Löb Logic) के लिए एक PSPACE-इष्टतम प्रमाण-खोज एल्गोरिदम प्रस्तुत करता है जो वाक्यात्मक निर्णयक्षमता (syntactic decidability) और जटिलता के संबंध में खुले प्रश्नों को हल करता है, जबकि रैखिक नेस्टेड सीक्वेंट्स (linear nested sequents) के साथ एक संबंध स्थापित करता है और परिमित प्रति-प्रतिमानों (finite counter-models) को निकालने के लिए एक तंत्र प्रदान करता है।

Tim S. Lyon, Omar Taher2026-06-03
🤖 AI

Towards Non-Monotonic Entailment in Propositional Defeasible Standpoint Logic

यह शोधपत्र प्रोपोज़िशनल डिफ़ीज़ेबलल स्टैंडपॉइंट लॉजिक (PDSL) को सिचुएटेड स्टैंडपॉइंट कंडिशनल्स के साथ विस्तारित करने की एक विधि प्रस्तावित करता है ताकि पारंपरिक KLM-शैली के तर्क से नॉन-मोनोटोनिक रेशनल एंटेलमेंट संबंधों को ऊपर उठाया जा सके, जिससे प्रोपोज़िशनल कॉम्प्लेक्सिटी बाउंड्स को सुरक्षित रखते हुए रेशनल और लेक्सिकोग्राफिक क्लोजर जैसी इन्फरेंस विधियों का निष्ठापूर्ण अनुवाद सक्षम हो सके।

Nicholas Leisegang, Thomas Meyer, Ivan Varzniczak2026-06-03
💻 computer science

Ranked MSO-enumeration over compressed words

यह शोध पत्र व्याकरण-संकुचित (grammar-compressed) स्ट्रिंग्स पर रैंक किए गए MSO-क्वेरी एन्यूमरेशन के लिए पहले एल्गोरिदम को प्रस्तुत करता है, जो संकुचित सेटिंग के अनुकूल फैक्टरिज़ेशन ट्री (factorization trees) को अपनाकर रैखिक प्रीप्रोसेसिंग और निरंतर विलंब (constant delay) प्राप्त करता है, जो तत्पश्चात संकुचित इनपुट पर पॉलीरेगुलर फलनों (polyregular functions) के कुशल एन्यूमरेशन को सक्षम बनाता है।

Markus Lohrey2026-06-03
💻 computer science

The TPTP Format for Interpretations

यह शोधपत्र टार्स्कियन (Tarskian), हर्ब्रैंड (Herbrand) और क्रिप्की (Kripke) व्याख्याओं को निरूपित करने के लिए TPTP प्रारूप का परिचय और विवरण प्रस्तुत करता है, जिसमें विभिन्न अनुप्रयोगों के लिए इसकी पर्याप्तता सुनिश्चित करने हेतु इसके सिंटैक्स, सिमेंटिक्स, सत्यापन और टूल सपोर्ट को शामिल किया गया है।

Geoff Sutcliffe, Alexander Steen, Pascal Fontaine, Lydia Kondylidou2026-06-02
💻 computer science

The memory of ω\omega-regular and BC(Σ20\Sigma_2^0) objectives

यह शोधपत्र स्थापित करता है कि ω\omega-रेगुलर उद्देश्यों के लिए आवश्यक मेमोरी की गणना NP में की जा सकती है और यह परिमित एवं अनंत खेलों के लिए समान है, जबकि साथ ही यह भी सिद्ध करता है कि दो BC(Σ20\Sigma_2^0) उद्देश्यों के संघ की मेमोरी उनकी व्यक्तिगत मेमोरी के गुणनफल द्वारा सीमित है, और ये परिणाम क्रोमैटिक मेमोरी (chromatic memory) तक विस्तारित होते हैं।

Antonio Casares, Pierre Ohlmann2026-06-02
🔢 mathematics

On Effective Banach-Mazur Games and an application to the Poincaré Recurrence Theorem for Category

यह शोध पत्र प्रभावी प्रथम श्रेणी (effective first category) के समुच्चयों को अभिलक्षणित करने के लिए बानाच-माज़ुर खेल (Banach-Mazur game) के एक प्रभावी संस्करण को प्रस्तुत करता है, जिसका उपयोग फिर प्रभावी बानाच श्रेणी प्रमेय (effective Banach Category Theorem) को सिद्ध करने और श्रेणी के लिए एक प्रभावी पोइनकारे पुनरावृत्ति प्रमेय (Poincaré Recurrence Theorem) स्थापित करने के लिए किया जाता है।

Prajval Koul, Satyadev Nandakumar2026-06-02