1090 पेपर
यह शोध पत्र यह प्रदर्शित करता है कि शुद्ध -कैलकुलस (lambda-calculus) टैबलिंग (tabling) पर आधारित एक नई परिचालन अर्थविज्ञान (operational semantics) के माध्यम से चक्रीय ग्राफ (cyclic graphs), स्वचालित डायनेमिक प्रोग्रामिंग और परिमित-समय लूप डिटेक्शन को मूल रूप से समर्थन दे सकता है, जिससे बाहरी पुनरावृत्ति संरचनाओं या अशुद्ध मेमोइज़ेशन (memoization) की आवश्यकता समाप्त हो जाती है।
यह शोध पत्र AI-संचालित MechMath एजेंट टीम द्वारा उत्पन्न और Lean में सत्यापित, OEIS A080170 मानदंड का एक औपचारिक प्रमाण प्रस्तुत करता है, जो यह स्थापित करता है कि विशिष्ट द्विपद गुणांकों (binomial coefficients) का महत्तम समापवर्तक (greatest common divisor) एक के बराबर होता है यदि और केवल यदि का उसके सबसे बड़े अभाज्य-घात कारक (prime-power factor) द्वारा भागफल उस कारक से अधिक हो।
यह शोध पत्र पॉइंट ट्रांज़िशन सिस्टम्स पर आधारित एक नए प्रकार के प्रूफ़ स्कीमा (proof schema) को प्रस्तुत करता है जो इंडक्टिव प्रूफ़्स के लिए हर्ब्रैंड सिस्टम्स (Herbrand systems) की गणना करने में सक्षम बनाता है, साइक्लिकिक प्रूफ़्स से इन स्कीमा में एक रूपांतरण स्थापित करता है, और 2-हाइड्रा (2-Hydra) कथन को सिद्ध करके उनकी उत्कृष्ट अभिव्यंजक शक्ति का प्रदर्शन करता है, जो मानक LKID में अप्रमाणित है।
यह शोध पत्र अनिश्चित प्राथमिकताओं वाले ASPIC तर्क ढांचों (argumentation frameworks) की अभिव्यंजक शक्ति की जांच करता है, यह प्रदर्शित करते हुए कि अमूर्त औपचारिकताओं (abstract formalisms) के साथ अधिकांश तुलनाएं नकारात्मक परिणाम देती हैं, और साथ ही उनकी अभिव्यंजक क्षमता के लिए एक गैर-तुच्छ सीमा (non-trivial threshold) के संबंध में एक अनुमान प्रस्तावित और आंशिक रूप से मान्य करता है।
यह शोध पत्र प्रथम-क्रम तर्क (फर्स्ट-ऑर्डर लॉजिक) के एक सिंटैक्टिक वेरिएंट के लिए एक रैंक-संरक्षण स्थानीयता प्रमेय (rank-preserving locality theorem) स्थापित करता है, जो अधिक कुशल मूल्यांकन के लिए कमजोर स्कैटर वाक्यों (weak scatter sentences) को शामिल करता है, जिसे विशेष रूप से सीमित मर्ज-चौड़ाई (bounded merge-width) वाले ग्राफों पर लागू किया गया है।
यह शोध पत्र चार स्वयंसिद्ध अभिधारणाओं (axiomatic postulates) का प्रस्ताव करके और यह सिद्ध करके कि संभाव्य एब्स्ट्रैक्ट स्टेट मशीन्स (pASMs) व्यवहारिक तुल्यता के साथ इन अभिधारणाओं को संतुष्ट करने वाले किसी भी एल्गोरिदम का अनुकरण कर सकते हैं, संभाव्य एल्गोरिदम का एक व्यवहारिक सिद्धांत स्थापित करता है।
यह शोध पत्र एक नए कंपोजिशनल (compositional) भाषा का प्रस्ताव करके मानकीकृत ग्राफ क्वेरी भाषाओं GQL और SQL/PGQ में संरचनात्मकता (compositionality) की कमी को संबोधित करता है, जो अभिव्यक्ति के अंतराल को पाटने और नए ग्राफ तत्वों के निर्माण को सक्षम करने के लिए रेगुलर पाथ क्वेरीज़ को एक पूर्णतः कंपोजिशनल ग्राफ-टू-ग्राफ #Datalog एक्सटेंशन के साथ जोड़ती है।
यह शोधपत्र ऑपरेंड्स को टाइप करने वाले एक सॉर्ट-स्ट्रैटिफाइड (sort-stratified) सिमेंटिक्स को पेश करके, इंस्टेंट्स (instants) और ड्यूरेशन्स (durations) के बीच अस्पष्ट तुलना ऑपरेटरों के कारण ODRL नीतियों में होने वाली टेम्पोरल कॉन्फ्लिक्ट डिटेक्शन की अनसाउंडनेस (unsoundness) को संबोधित करता है, जो कॉन्फ्लिक्ट चेकिंग को तीन-मूल्य वाले वर्डिक्ट (three-valued verdict) के साथ इंटरवल तुलना में कम करता है, और स्टैटिक एवं रनटाइम इवैल्यूएशन के माध्यम से इसकी डैसिडेबिलिटी (decidability) और साउंडनेस को सिद्ध करता है।
यह शोध पत्र एक ऐसे स्वचालित उपकरण के लिए सैद्धांतिक आधार प्रस्तुत करता है जो उपयोगकर्ता द्वारा प्रदान की गई अंतर्दृष्टि को एक नवीन उच्च-क्रम अमूर्त व्याख्या (higher-order abstract interpretation) तकनीक के साथ जोड़कर तर्क एल्गोरिदम (reasoning algorithms) की जटिलता का विश्लेषण करता है, जिससे पुनरावृत्ति समीकरणों (recurrence equations) को निकाला जाता है, जिन्हें फिर प्री/पोस्टपॉइंट-आधारित विधियों और एसएमटी (SMT) सॉल्वर्स का उपयोग करके हल और सत्यापित किया जाता है।
यह शोध पत्र सुव्यवस्थित (well-typed) पदों के लिए एक ग्लोबल ट्रेस कंडीशन (GTC) के साथ इन्फिनिटरी लैम्ब्डा कैलकुलस के एक विस्तार को प्रस्तुत करता है, जो यह सिद्ध करता है कि ऐसे पद प्रबल रूप से अभिसारी अनंत न्यूनीकरण (strongly convergent infinite reductions) प्रदर्शित करते हैं, संख्यात्मकों (numerals) में न्यूनीकृत होते हैं, और गॉडेल के सिस्टम टी (Gödel's System T) के पूर्ण फलनों (total functions) को अभिलक्षित करते हैं।