1105 पेपर
यह शोध पत्र पुनरावृत्ति-मुक्त (recursion-free) प्रोग्रामों को संश्लेषित करने के लिए एक परिष्कृत सुपरपोजिशन-आधारित कलन (calculus) प्रस्तुत करता है जो ध्वनि और पूर्ण (sound and complete) सिद्ध है, जो यह गारंटी देता है कि जब भी कोई गणनीय समाधान मौजूद हो, तो उसकी खोज सुनिश्चित की जा सकेगी।
यह शोध पत्र यह स्थापित करता है कि रैखिक योजनाओं (linear plans) पर 'जानने-कैसे' (knowing-how) कथनों को व्यक्त करने वाले एक मोडल लॉजिक के लिए संतोषजनकता समस्या (satisfiability problem) NP-कम्प्लीट है, जो कि समस्या को मोडल लॉजिक S5 में अनुवादित करके प्राप्त किया गया एक परिणाम है।
यह शोध पत्र अरस्तू (Aristotle) API का उपयोग करके IMO 2009 ग्रासहॉपर (Grasshopper) समस्या के एक लीन 4 (Lean 4) औपचारिकीकरण केस स्टडी को प्रस्तुत करता है, जो यह प्रदर्शित करता है कि यद्यपि AI प्रमाण रणनीति के स्थानीय घटकों को सफलतापूर्वक सत्यापित कर सकता है, लेकिन यह मुख्य प्रमेय को पूर्ण करने के लिए आवश्यक वैश्विक संयोजी बहीखाता पद्धति (global combinatorial bookkeeping) को हल करने में वर्तमान में संघर्ष करता है।
यह शोध पत्र दीर्घकालिक पावर ग्रिड नियोजन को अनुकूलित करने के लिए उत्तर सेट प्रोग्रामिंग (ASP) का उपयोग करने वाले पहले स्वचालित दृष्टिकोण का प्रस्ताव करता है, जो सिंथेटिक और वास्तविक दुनिया के डेटा दोनों पर प्रयोगों के माध्यम से जटिल टोपोलॉजिकल और कॉम्बिनेटोरियल बाधाओं को संभालने में इसकी प्रभावशीलता को प्रदर्शित करता है।
यह शोधपत्र यह स्थापित करता है कि किसी भी बाधा संतुष्टि समस्या (CSP) के उदाहरण को उसकी गैर-अनावश्यकता (या भारित मामलों के लिए श्रृंखला लंबाई) के आनुपातिक आकार तक विरल बनाया जा सकता है, जो यह सिद्ध करता है कि सन्निकटन के लिए अनावश्यक उपवाक्य पर्याप्त हैं, यह परिणाम एंट्रॉपी पद्धति और कोडिंग सिद्धांत तकनीकों के नवीन अनुप्रयोगों के माध्यम से प्राप्त किया गया है जो CSP विरलीकरण की सीमाओं को सटीक रूप से निर्धारित करते हैं।
यह शोध पत्र स्थापित करता है कि गार्डेड नेगेशन ट्रांजिटिव क्लोजर लॉजिक (GNTC) के लिए संतुष्टि समस्या (satisfiability problem) 2ExpTime-complete है और इसकी मॉडल चेकिंग समस्या -complete है, जिससे यूनरी नेगेशन फ्रैगमेंट (UNTC) और दोनों के लिए पूर्व में खुले जटिलता संबंधी प्रश्नों का समाधान होता है।
यह शोध पत्र प्रदर्शित करता है कि एक लैमिनर सेट सिस्टम (laminar set system) के अनुरूप लैमिनर ट्री (laminar tree) का निर्माण मोनैडिक सेकंड-ऑर्डर लॉजिक (MSO) ट्रांसडक्शन के माध्यम से किया जा सकता है, जिससे कुरसेल (Courcelle) का एक खुला प्रश्न हल होता है और उन विभिन्न ग्राफ डिकम्पोज़िशन (graph decompositions) की MSO-आधारित व्युत्पत्ति सक्षम होती है जिनके लिए पूर्व में काउंटिंग क्वांटिफायर (counting quantifiers) की आवश्यकता थी, साथ ही ऐसे सिस्टम पर MSO के भीतर इन क्वांटिफायर के अनुकरण की सीमाओं का भी अन्वेषण किया जाता है।
यह शोध पत्र ल्यूस्ट्र (Lustre) मॉडल चेकिंग और स्थानीय खोज (local search) के साथ संबंधों का लाभ उठाकर, सी-रास्प (C-RASP) प्रोग्रामों—जो ट्रांसफॉर्मर अभिव्यक्तता को समाहित करने वाले भाषा निर्माण हैं—को स्वचालित रूप से सत्यापित करने और सीखने के लिए नई एल्गोरिद्मिक तकनीकों को प्रस्तुत करता है, जिससे ट्रांसफॉर्मर प्रोग्राम अनुकूलन और बाधित शिक्षण (constrained learning) में अनुप्रयोग सक्षम होते हैं।
यह शोध पत्र हाइपरएलिप्टिक डायोफैंटाइन समीकरणों और निम्न-जीनस (low-genus) बीजगणितीय वक्रों के परिणामों का लाभ उठाते हुए पूर्ण निश्चित घातों (perfect fixed powers) और त्रिघातीय बहुपदों (cubic polynomials) के लिए प्रेसबर अंकगणित (Presburger arithmetic) के एकल-चर विस्तारों की निर्णयक्षमता (decidability) स्थापित करता है, जबकि यह प्रदर्शित करता है कि इन प्रतिबंधों को हटाने से ओपन डायोफैंटाइन समस्याओं के एन्कोडिंग के माध्यम से अनिश्चितता (undecidability) उत्पन्न होती है।
यह शोध पत्र GRASS प्रस्तुत करता है, जो एक एकीकृत प्रकार प्रणाली (unified type system) है जो सब्स्ट्रक्चरल लॉजिक के रिसोर्स रिस्ट्रिक्शन तंत्र को ग्रेडेड सिस्टम्स की क्वांटिटेटिव ट्रैकिंग के साथ एकीकृत करता है, जिससे एक ही ढांचे के भीतर वेरिएबल यूसेज पर लचीला, हेटेरोजेनियस नियंत्रण सक्षम होता है और अपने कैटेगोरिकल सेमैंटिक्स के माध्यम से LNL, एडजॉइंट लॉजिक और mGL जैसे स्थापित मॉडलों को समाहित करता है।