cs.LO पेपर | Gist.Science

Basic Model Theory for Path Predicate Modal Logic

यह शोध पत्र पाथ प्रेडिकेट मोडल लॉजिक (PPML) के बुनियादी मॉडल-सैद्धांतिक पहलुओं की जांच करता है, जो डेटा-जागरूक औपचारिकताओं का अमूर्त रूप से विश्लेषण करने के लिए डिज़ाइन किया गया बेसिक मोडल लॉजिक का एक सामान्यीकरण है, जिसमें हेनेसी-मिलनर वर्गों (Hennessy-Milner classes) का अन्वेषण किया गया है और इसकी अभिव्यंजक शक्ति को बेहतर ढंग से समझने के लिए एक वैन बंटम लक्षण वर्णन प्रमेय (van Benthem characterization theorem) स्थापित किया गया है।

Raul Fervari (CONICET,Universidad Nacional de Cordoba Argentina), Santiago Figueira (CONICET,Universidad de Buenos Aires (…)2026-07-23

💻 computer science

MaudeTypedLog: A Typed Interpreter for Prolog in Maude

यह शोधपत्र MaudeTypedLog प्रस्तुत करता है, जो Maude में कार्यान्वित एक Prolog इंटरप्रेटर है जो प्रोग्राम और क्वेरी दोनों में टाइप एरर (type errors) का गतिशील रूप से पता लगाने के लिए एक टाइप्ड यूनिफिकेशन एल्गोरिदम (typed unification algorithm) और टाइप्ड SLD-रिज़ॉल्यूशन (Typed SLD-resolution) का उपयोग करता है।

Enrique Gallifa-Tronch (Valencian Research Institute for Artificial Intelligence), João Barbosa (DCC, Faculdade de Ciênc (…)2026-07-23

💻 computer science

Robust Classification in ML: A Topological Semantics Approach

यह शोध पत्र टोपोलॉजिकल सिमेंटिक्स (topological semantics) पर आधारित एक सुदृढ़ वर्गीकरण के लिए एक तार्किक ढांचे का प्रस्ताव करता है, जो स्थानीय सत्य निरंतरता (local truth persistence) और वैश्विक समावेशन संबंधों (global inclusion relations) को औपचारिक रूप से चित्रित करने के लिए एक रोबस्टनेस मोडैलिटी (robustness modality) और एक कंडिशनल कनेक्टिव (conditional connective) के साथ एक सुदृढ़ और पूर्ण मोडल लॉजिक पेश करता है, साथ ही क्लासिफायर व्यवहार का विश्लेषण और व्याख्या करने के लिए मिनिमल रोबस्ट मॉडल्स (Minimal Robust Models) उत्पन्न करने की एक रचनात्मक विधि प्रस्तुत करता है।

Dominik Pichler (TU Wien), Mirko Tagliaferri (TU Wien)2026-07-23

💻 computer science

From Dag-Like Proofs to Boolean Circuits in Lean

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

Lorenzo Saraiva (Pontificia Universidade Catolica do Rio de Janeiro), Edward Hermann Haeusler (Pontificia Universidade C (…)2026-07-23

💻 computer science

Phase Semantic Cut-elimination for Intuitionistic Linear Logic with Least and Greatest Fixed Points

यह शोध पत्र न्यूनतम और उच्चतम फिक्स्ड पॉइंट्स ( $\mu$ IMALL) वाले इंट्यूशनिस्टिक प्रोपोज़िशनल मल्टीप्लिकेटिव-एडिटिव लीनियर लॉजिक के लिए अपने फेज सिमेंटिक्स को परिभाषित करके और साउंडनेस एवं कट-फ्री पूर्णता दोनों को सिद्ध करके कट-एलिमिनेशन प्रमेय स्थापित करता है।

Jun Suzuki (Hokkaido University), Charles Grellois (University of Sheffield), Katsuhiko Sano (Hokkaido University)2026-07-23

💻 computer science

A Machine-checked Proof of Consistency for Impredicative Pure Type Systems

यह शोध पत्र टाइप थ्योरी के मशीनीकरण को आगे बढ़ाने के लिए क्लासिकल सिंटैक्स, स्टौटनटन के मल्टीपल सब्स्टिट्यूशन और अल्फा-कम्यूटेटिव रिलेशंस के एक नवीन सिद्धांत का उपयोग करते हुए, इम्प्रेडिकेटिव प्योर टाइप सिस्टम्स के लिए कन्फ्लुएंस, सब्जेक्ट रिडक्शन और कंसिस्टेंसी का Agda में एक मशीन-चेक्ड प्रूफ प्रस्तुत करता है।

Sebastián Urciuoli (Universidad ORT Uruguay)2026-07-23

💻 computer science

Connectivity at the crossroad of intuitionistic and classical polarizations in linear logic

यह शोध पत्र मल्टीप्लिकेटिव एक्सपोनेंशियल लीनियर लॉजिक के VMELL खंड को प्रस्तुत करता है, जो शास्त्रीय और इंट्यूशनिस्टिक ध्रुवीकरणों को एकीकृत करता है और डैनोस-रेनियर विशेषता का विस्तार करके प्रूफ़-नेट्स के माध्यम से बैंग कैलकुलस टर्म्स को निरूपित करने हेतु एक गणनात्मक रूप से कुशल शुद्धता मानदंड स्थापित करता है।

Raffaele Di Donna, Giulio Guerrieri, Lorenzo Tortora de Falco2026-07-23

💻 computer science

A Compositional Approach to Verifying Modular Robotic Systems

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

Matt Luckcuck, Marie Farrell, Angelo Ferrando, Rafael C. Cardoso, Louise A. Dennis, Michael Fisher2026-07-22

🔢 mathematics

The equational theory of the Weihrauch lattice with (iterated) composition

यह शोध पत्र घटक (composition) और पुनरावृत्ति (iteration) के साथ विस्तारित वीह्राउच लैटिस (Weihrauch lattice) के निर्णय योग्य समीकरण सिद्धांत (decidable equational theory) को परिमित ग्राफ़ पर बुची गेम्स (Büchi games) का उपयोग करके अभिलक्षित करता है, जो क्लीनी बीजगणित (Kleene algebras) के समान एक पूर्ण अभिलेखन (axiomatization) प्रदान करता है और वैधता समस्या (validity problem) के लिए PSPACE-कठोरता (PSPACE-hardness) स्थापित करता है।

Cécilia Pradic2026-07-22

💻 computer science

Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic

यह शोध पत्र मोंटेग्यू और गैलिन की प्रणाली का सामान्यीकरण करते हुए सरल-टाइप्ड कॉन्स्टेंट-डोमेन मोडल लैम्ब्डा कैलकुलस $\boldsymbol{\lambda}_\theta$ को विकसित करता है ताकि $\mathsf{BCKW}$ -आधारित कॉम्बिनेटरी लॉजिक के माध्यम से एक एंड्रयूज-समान लक्षण वर्णन, मैक्सिमल और ऑर्डिनरी प्रणालियों के साथ सिमेंटिक संरक्षण और अभिव्यक्तता संबंध, और कॉम्बिनेटरी लॉजिक तथा वीक डीडक्टिव सिस्टम्स के बीच एक आंशिक पत्राचार स्थापित किया जा सके जो ज़िमरमैन द्वारा उठाए गए एक प्रश्न का उत्तर देता है।

Sean Walsh2026-07-22

← पिछला अगला →