1105 पेपर
यह शोधपत्र अनिश्चितता वाले दो-खिलाड़ी बारी-बारी से चलने वाले जनरल गेम डिस्क्रिप्शन लैंग्वेज (GDL) खेलों को हल करने के लिए पहले ASP-आधारित दृष्टिकोण के रूप में स्टोकेस्टिक आंसर सेट प्रोग्रामिंग (SQASP) को प्रस्तुत करता है, जो छोटे स्टोकेस्टिक खेलों पर फॉरवर्ड सर्च के साथ इसकी प्रतिस्पर्धात्मकता और एंडगेम मूल्यांकन की इसकी क्षमता को प्रदर्शित करता है।
यह शोध पत्र समानता भाषाओं (equality languages) पर क्वांटिफाइड कंस्ट्रेंट सैटिस्फिएबिलिटी प्रॉब्लम (QCSP) के लिए एक पूर्ण जटिलता त्रिक विभाजन (Logspace, NP-complete, या PSpace-complete) स्थापित करता है, जो यह सिद्ध करके कि QCSP PSpace-complete है, और साथ ही सीमित परिवर्तनशीलता (bounded alternation) वाले संस्करण को पॉलीनोमियल हाइरार्की (Polynomial Hierarchy) के भीतर वर्गीकृत करता है।
यह शोध पत्र सिद्ध करता है कि फीचर कोलीनियैरिटी (feature collinearity) के तहत कोई भी फीचर रैंकिंग विधि एक साथ फथफुलनेस (faithfulness), स्टेबिलिटी (stability) और कम्प्लीटनेस (completeness) प्राप्त नहीं कर सकती, जो परिणामी डिज़ाइन स्पेस को अस्थिर फथफुल विधियों और DASH जैसे स्थिर एन्सेम्बल दृष्टिकोणों के बीच एक सख्त द्विभाजन के रूप में अभिलक्षणित करता है, और सभी निष्कर्षों को Lean 4 में यांत्रिक रूप से सत्यापित किया गया है।
यह शोध पत्र शून्य विशेषता (characteristic zero) में ऑर्बिट गणनाओं और परिमित शब्दावलियों (finite vocabularies) में मुक्त समामेलन (free amalgamation) पर आधारित स्थितियाँ स्थापित करके, रैडो ग्राफ (Rado graph) सहित अनंत संरचनाओं के एक विस्तृत वर्ग तक गणनीय शुद्ध समुच्चय (countable pure set) और सघन रैखिक क्रम (dense linear order) के परिमित लंबाई गुण का सामान्यीकरण करता है, साथ ही फलन स्थानों (function spaces) और ऑटोमेटा के साथ संबंधों का भी अन्वेषण करता है।
यह शोध पत्र पैरामीट्रिक मॉड्यूलर लॉजिक प्रोग्राम्स को प्रथम-क्रम (first-order) आंसर सेट प्रोग्रामिंग के एक नए औपचारिक रूप (formalism) के रूप में प्रस्तुत करता है जो पैरामीटर्स और इंटेंशनलिटी (intensionality) का समर्थन करता है, जिससे clingo की कलेक्टिव कंट्रोल विशेषता के अर्थविज्ञान (semantics) को पकड़ने और मॉड्यूलर एवं पारंपरिक गैर-मॉड्यूलर ASP के बीच के अंतर को पाटने के लिए एक सैद्धांतिक आधार प्राप्त होता है।
यह शोध पत्र गणनीय तार्किक संरचनाओं (countable logical structures) पर इक्विवैरिएंट बहुपद आदर्शों (equivariant polynomial ideals) के परिमित पीढ़ी (finite generation) के लिए आवश्यक और पर्याप्त स्थितियाँ स्थापित करता है और उनके ग्रोबनर आधार (Gröbner bases) की गणना करने के लिए एक विस्तारित बुचबर्गर एल्गोरिदम (Buchberger's algorithm) विकसित करता है, जिससे सदस्यता समस्या (membership problem) हल होती है और रजिस्टर ऑटोमेटा (register automata) तथा डेटा के साथ पेट्री नेट (Petri nets with data) जैसे क्षेत्रों में अनुप्रयोग संभव होते हैं।
यह शोध पत्र एक अफ़ाइन उच्च-क्रम मात्रात्मक तर्क (affine higher-order quantitative logic) प्रस्तुत करता है जो $1$-बद्ध पूर्ण मीट्रिक स्थानों (1-bounded complete metric spaces) और प्रायिकता मापों (probability measures) के लिए नवीन आगमन (induction) और गार्ड की गई पुनरावृत्ति (guarded recursion) सिद्धांतों से सुसज्जित है, जो बिसिमिलरिटी दूरियों (bisimilarity distances), टेम्पोरल लर्निंग कन्वर्जेंस (temporal learning convergence) और रैंडम वॉक (random walks) पर केस स्टडीज के माध्यम से प्रायिक कार्यक्रमों और प्रक्रियाओं के सत्यापन में इसकी उपयोगिता को प्रदर्शित करता है।
यह शोध पत्र \textsc{CB-Ver} को प्रस्तुत करता है, जो एक मॉड्यूलर फ्रेमवर्क है जो समानांतर SMT-आधारित घटक जाँचों और Lean में औपचारिक साउंडनेस प्रमाणों के माध्यम से एक "कनवर्जेस-बिफोर ग्राफ" को संश्लेषित और मान्य करके अंततः-स्थिर नेटवर्क कंट्रोल प्लेन गुणों को सत्यापित करता है, साथ ही वांछित शुद्धता गुणों से घटक इंटरफेस के स्वचालित निर्माण को भी सक्षम बनाता है।
यह शोध पत्र एक औपचारिक सत्यापन ढांचा प्रस्तुत करता है जो सीएनसी (CNC) वर्कस्पेस को एक स्थानिक हीप (spatial heap) के रूप में मॉडल करता है और भौतिक टकरावों का पता लगाने के लिए सेपरेशन लॉजिक (Separation Logic) को तार्किक डेटा रेस (logical data races) के रूप में लागू करता है, जिससे सुरक्षित, स्वायत्त विनिर्माण के लिए पुनरावृत्ति सिमुलेशन पर निर्भरता कम होती है।
लीन रिफैक्टर (Lean Refactor) एक रिट्रीवल-ऑगमेंटेड एजेंटिक फ्रेमवर्क है जो बिना किसी मॉडल रिट्रेनिंग के, क्यूरेटेड रिफैक्टरिंग रणनीतियों को गतिशील रूप से चुनकर टोकन कंप्रेशन, कंपाइलेशन स्पीड और वर्जन कम्पैटिबिलिटी सहित कई उद्देश्यों के लिए लीन (Lean) प्रूफ को अनुकूलित करता है।