💻 Category

cs.LO

1086 पेपर

💻 computer science

Barbed Similarity for the π\pi-Calculus in Beluga: A Case Study in Coinductive Reasoning

यह शोध पत्र बेलुगा (Beluga) प्रूफ असिस्टेंट में रेप्लिकेशन (replication) के साथ π\pi-कैलकुलस के लिए स्ट्रॉन्ग बारब्ड सिमिलरिटी (strong barbed similarity) के एक औपचारिकीकरण को प्रस्तुत करता है, जो यह प्रदर्शित करता है कि कैसे बेलुगा का कोपैटर्न-आधारित कोइंडक्शन (copattern-based coinduction) और हायर-ऑर्डर एब्स्ट्रैक्ट सिंटैक्स (higher-order abstract syntax), व्यवहारिक तुल्यता (behavioral equivalence) और कॉन्टेक्स्ट लेम्मा (context lemmas) के संक्षिप्त और कंपोजिशनल प्रमाणों को सक्षम बनाता है।

Lea Trogni (Dipartimento di Matematica, Università degli Studi di Milano, Italy), Gabriele Cecilia (School of Computer,C (…)2026-07-15
💻 computer science

Proof Theory and Dependent Type Theory: Distinct Foundations for Designing Proof Assistants

यह शोध पत्र तर्क देता है कि आधुनिक संरचनात्मक प्रमाण सिद्धांत (structural proof theory), जिसका उदाहरण सीक्वेंट कैलकुलस (sequent calculus) है और जिसे एबेला (Abella) थ्योरम प्रूवर में कार्यान्वित किया गया है, तर्क को प्रमाण संरचना से बेहतर ढंग से अलग करने, गैर-निर्धारणवाद (non-determinism) का रणनीतिक उपयोग करने, जटिल टाइपिंग संबंधी समस्याओं से बचने और बाइंडिंग्स (bindings) को संभालने के लिए एक सुरुचिपूर्ण दृष्टिकोण प्रदान करने के माध्यम से, प्रूफ असिस्टेंट्स को डिजाइन करने के लिए डिपेंडेंट टाइप थ्योरी (dependent type theory) का एक सम्मोहक विकल्प प्रस्तुत करता है।

Dale Miller (Inria Saclay,LIX, Institut Polytechnique de Paris)2026-07-15
💻 computer science

Anti-Unification Completeness Analysis in PVS

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

Mauricio Ayala-Rincón (Universidade Federal de Goiás), Thaynara Arielly de Lima (Universidade Federal de Goiás), Maria J (…)2026-07-15
💻 computer science

Work-in-Progress: A Tactic for Pattern Matching in Autosubst

यह कार्य-प्रगति (work-in-progress) पत्र Autosubst के लिए एक स्वचालित पैटर्न मिलान टैक्टिक पेश करता है जो टाइपिंग नियमों, रिडक्शन संबंधों और गैर-अद्वितीय समाधानों को संभालने में इसकी वर्तमान सीमाओं को संबोधित करता है, जैसा कि POPLMark और POPLMark Reloaded चुनौतियों पर मूल्यांकनों के माध्यम से प्रदर्शित किया गया है।

Mathews George (Heriot-Watt University Edinburgh), Kathrin Stark (Heriot-Watt University Edinburgh)2026-07-15
💻 computer science

A Strategy Language for Controlled Proof Search

यह शोधपत्र Pgeon को प्रस्तुत करता है, जो एक मेटा-प्रूवर (meta-prover) है जिसमें एक स्ट्रैटेजी लैंग्वेज (strategy language) है जो अनुक्रमिक संयोजन (sequential composition), विकल्प (choice) और इंटरलीविंग (interleaving) जैसे ऑपरेटरों के माध्यम से अर्ध-निर्णय योग्य लॉजिक्स (semi-decidable logics) में निष्पक्ष और पूर्ण अन्वेषण सुनिश्चित करने के लिए अनुमान नियमों (inference rules) को प्रूफ़ सर्च (proof search) से अलग करती है।

Romain Sidhoum (LIRMM, Univ. Montpellier, CNRS, Montpellier, France), Simon Robillard (LIRMM, Univ. Montpellier, CNRS, M (…)2026-07-15
💻 computer science

MaxSAT-Based Feedback for Guiding Vision-Language Models in Sudoku

यह शोध पत्र एक न्यूरो-सिम्बोलिक ढांचे का प्रस्ताव करता है जो सुडोकू पहेलियों पर विजन-लैंग्वेज मॉडल्स के प्रदर्शन को बढ़ाने के लिए एक मैक्ससैट (MaxSAT) ओरेकल का उपयोग करता है ताकि संभावित असाइनमेंटों को मान्य किया जा सके और संरचित फीडबैक प्रदान किया जा सके, जिससे तार्किक निरंतरता लागू होती है और समाधान की सटीकता में सुधार होता है।

Pedro Orvalho, Guillem Alenyà, Felip Manyà2026-07-15
🔢 mathematics

Constraint satisfaction problems, compactness and non-measurable sets

यह शोध पत्र यह स्थापित करता है कि एक परिमित संबंधात्मक संरचना (finite relational structure) की कॉम्पैक्टनेस ज़र्मेलो-फ्रेंकेल सेट थ्योरी के भीतर तभी सिद्ध की जा सकती है जब उस संरचना की चौड़ाई एक हो, जबकि उच्च चौड़ाई वाली संरचनाओं के लिए इसकी कॉम्पैक्टनेस हेतु त्रि-आयामी स्थान में गैर-मापन योग्य समुच्चयों (non-measurable sets) का अस्तित्व आवश्यक है।

Claude Tardif2026-07-14
💻 computer science

North-East Lattice Paths Avoiding kk Collinear Points via Satisfiability

यह शोध पत्र k≤6k \leq 6 के लिए kk संरेखीय बिंदुओं (collinear points) से बचने वाले सभी उत्तर-पूर्व जालक पथों (north-east lattice paths) को सूचीबद्ध करने के लिए संतुष्टि समाधानकर्ताओं (satisfiability solvers) का उपयोग करता है और 7 संरेखीय बिंदुओं से बचने वाले 327 चरणों के एक नए रिकॉर्ड-तोड़ने वाले पथ की खोज करता है, जो पिछले सर्वश्रेष्ठ 260 चरणों से अधिक है।

Aaron Barnoff, Curtis Bright2026-07-14
🤖 AI

Referential Regimes: Transformation-Invariant Identity for Neutral Substrates

यह शोध पत्र तर्क देता है कि निरंतर असहमति द्वारा अभिलक्षित डेटा प्रणालियों में, एक तटस्थ आधार (न्यूट्रल सबस्ट्रेट) को कम से कम नौ रूपांतरण-अपरिवर्तनीय पहचान व्यवस्थाओं (ट्रांसफॉर्मेशन-इनवेरिएंट आइडेंटिटी रिजीम्स) के बीच अंतर करना चाहिए—जो छह स्पष्ट संदर्भ प्रकारों से अधिक है—ताकि उन व्याख्यात्मक परंपराओं पर निर्भर किए बिना संदर्भ को संरचनात्मक रूप से स्थिर किया जा सके जो निरंतर संघर्ष का सामना नहीं कर सकतीं।

Denise M. Case2026-07-14
💻 computer science

Prismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4

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

Leni Aniva, Claire Wang2026-07-14