1115 पेपर
यह शोध पत्र मौजूदा प्रस्तावात्मक दृष्टिकोणों की सीमाओं को संबोधित करने के लिए संदर्भ-संवेदी भारों के साथ सिंटैक्स-संवेदनशील भाषा मॉडलों को एकीकृत करने वाले एक चार-स्तरीय पैरामीट्रिक मॉडल का प्रस्ताव करके, फर्स्ट-ऑर्डर लॉजिक तर्कों में समानता मापने के लिए एक व्यापक, स्वयंसिद्ध ढांचे (एक्सियोमैटिक फ्रेमवर्क) को प्रस्तुत करता है।
यह लीन 4-औपचारिक (Lean 4-formalized) शोध पत्र एक न्यूनतम फ्रंट-सीड कोहेरेंस पैकेज (minimal front-seed coherence package) द्वारा प्रमुख सिमेंटिक प्रमेयों को पुनः प्राप्त करने के लिए पर्याप्त सिद्ध करके और रीफाई (reify), रिफ्लेक्ट (reflect), तथा एप्लीकेशन (application) ऑपरेशन्स के लिए सटीक कोऑर्डिनेटवाइज आइडेंटिटीज (coordinatewise identities) के साथ स्पष्ट, पूर्णतः सत्यापित ग्लोबल फॉर्मूला प्रदान करके अनटाइप्ड लैम्ब्डा-कैलकुलस (untyped lambda-calculus) के लिए K-इन्फिनिटी होमोटोपी-मॉडल (K-infinity homotopy-model) को आगे बढ़ाता है।
यह शोध पत्र विटनेस्ड सिमेट्रिक चॉइस (witnessed symmetric choice) और एक इंटरप्रिटेशन ऑपरेटर द्वारा विस्तारित काउंटिंग वाले फिक्स्ड-पॉइंट लॉजिक की अभिव्यंजक क्षमता की जांच करता है, यह प्रदर्शित करते हुए कि बाद वाला FO-इंटरप्रेशंस के तहत क्लोजर में विफल होकर शक्ति बढ़ाता है और विटनेस्ड सिमेट्रिक चॉइस ऑपरेटर्स का नेस्टिंग CFI ग्राफ्स पर अभिव्यंजक क्षमता को बढ़ाता है।
यह शोधपत्र एक मेटा-मोडल लॉजिक (meta-modal logic) प्रस्तुत करता है जिसमें बिसिमिलर (bisimilar) अवस्थाओं पर परिमाणीकरण (quantifying) के लिए एक नई मोडैलिटी (modality) दी गई है, यह स्थापित करते हुए कि बिसिमुलेशन (bisimulations) को इस भाषा के भीतर परिभाषित किया जा सकता है, एक सुसंगत और पूर्ण अभिलेखन (sound and complete axiomatization) प्रदान करता है, मानक मोडल लॉजिक में अनुवाद के माध्यम से संतोषजनकता (satisfiability) की PSPACE-पूर्णता (PSPACE-completeness) को सिद्ध करता है, और सभी परिणामों को Isabelle/HOL का उपयोग करके सत्यापित करता है।
यह शोधपत्र कंस्ट्रेंड अज़म्प्शन-बेस्ड आर्गुमेंटेशन (CABA) प्रस्तुत करता है, जो एक नवीन रूपरेखा है जो ग्राउंड-ओनली निरूपणों की सीमाओं को दूर करने के लिए अनंत डोमेन पर कंस्ट्रेंड वेरिएबल्स को शामिल करके मानक ABA का विस्तार करती है, और साथ ही मौजूदा ABA सिमेंटिक्स का रूढ़िवादी रूप से सामान्यीकरण करने वाले नॉन-ग्राउंड सिमेंटिक्स को परिभाषित करती है।
यह शोध पत्र SAT सॉल्वर और इसिंग ऑप्टिमाइज़ेशन (Ising optimization) के लिए प्लांटेड-सॉल्यूशन बेंचमार्क के एक स्केलेबल और सत्यापन योग्य परिवार को प्रस्तुत करता है, जो पूर्णांक गुणनखंडन बाधाओं (integer factorization constraints) से व्युत्पन्न है, और जो कारकों के बिट-लेंथ के सापेक्ष घातीय रनटाइम वृद्धि प्रदर्शित करता है।
यह शोध पत्र LTLF को प्रस्तुत करता है, जो एक नवीन टेम्पोरल लॉजिक है जो इवेंट सीरीज़ के फ्रीक्वेंसी गुणों को औपचारिक रूप से व्यक्त करने, निगरानी करने और भविष्यवाणी करने के लिए मेजर-सेंसिटिव मोडल क्वांटिफायर और एक क्रिपके-शैली की सिमेंटिक्स से सुसज्जित है, जिससे मात्रात्मक प्रणालियों में तार्किक तर्क और अनुभवजन्य अवलोकन के बीच के अंतर को पाटा जा सके।
यह शोध पत्र सिद्धांतों को तौलने के लिए चैतिन के ह्यूरिस्टिक सिद्धांत (Chaitin's Heuristic Principle) को पुनर्जीवित करने का प्रयास करता है और साथ ही यह प्रदर्शित करता है कि चैतिन का स्थिरांक ओमेगा (Chaitin's constant Omega) किसी भी अनंत विविक्त माप (infinite discrete measure) के तहत एक रुकने की प्रायिकता (halting probability) नहीं है, तत्पश्चात रुकने की प्रायिकताओं को परिभाषित करने के लिए वैकल्पिक विधियों का प्रस्ताव करता है।
यह शोध पत्र हार्डवेयर-सॉफ्टवेयर अनुबंध संतुष्टि के मॉड्यूलर, संवादात्मक सत्यापन को सक्षम करने के लिए रिलेटिव बिसिमिलरेशन (relative bisimulation) और कोइंडक्टिव रीजनिंग (coinductive reasoning) पर आधारित एक सुदृढ़ और पूर्ण निगमनात्मक प्रमाण प्रणाली प्रस्तुत करता है, जैसा कि इसके रॉक (Rocq) प्रूफ़ असिस्टेंट में औपचारिकीकरण और चुनौतीपूर्ण सुरक्षा प्रमाणों पर इसके अनुप्रयोग द्वारा प्रदर्शित किया गया है।
यह शोधपत्र यह प्रदर्शित करता है कि पारंपरिक कार्टेशियन सिंटैक्स से आरेखीय मोनॉइडल ढांचे (diagrammatic monoidal framework) की ओर स्थानांतरित होकर, "नियो-पियर्सियन संबंधों के कलन" (calculus of neo-Peircean relations) को प्रस्तुत करके—जो प्रथम-क्रम तर्क (first-order logic) की अभिव्यक्तता प्राप्त करने के लिए कार्टेशियन और लीनियर बाइकैटेगरी को संयोजित करता है—संबंधों के पूर्ण कलन के लिए एक पूर्ण स्वयंसिद्धीकरण (axiomatisation) प्राप्त करना संभव है—जो पिछले 'नो-गो' सिद्धांतों (no-go theorems) का भी परिहार करता है।