1117 पेपर
यह शोध पत्र कैनोनिकल निरूपणों (canonical representations) का उपयोग करके खोज स्थान को सीमित करने के माध्यम से मास स्पेक्ट्रोमेट्री डेटा से आणविक संरचनाओं को निर्धारित करने के लिए एक नवीन आंसर सेट प्रोग्रामिंग (ASP) दृष्टिकोण प्रस्तुत करता है, जो मौजूदा सिमेट्री-ब्रेकिंग विधियों और वाणिज्यिक उपकरणों की तुलना में इसकी शुद्धता और बेहतर प्रदर्शन को प्रदर्शित करता है।
यह शोध पत्र probLO प्रस्तुत करता है, जो लीनियर लॉजिक प्रोग्रामिंग का एक विस्तार है जो संरचना पुनर्निर्माण के लिए मल्टी-हेड प्रोलॉग-समान विधियों और आंतरिक संख्यात्मक संभाव्यता गणनाओं के लिए लीनियर लॉजिक स्लाइसिंग का उपयोग करके बायेसियन नेटवर्क प्रतिनिधित्व और गणना को एकीकृत करता है।
यह शोध पत्र RCbr को प्रस्तुत करके विरोधाभासी विश्वास संशोधन (Paraconsistent Belief Revision) को आगे बढ़ाता है, जो Cbr तर्क का एक प्रतिस्थापन-समृद्ध विस्तार है, जो विरोधाभास के औपचारिक तर्कशास्त्र (Logics of Formal Inconsistency) के भीतर ज्ञान संबंधी दृढ़ता (epistemic entrenchment) पर आधारित विश्वास परिवर्तन तंत्रों के औपचारिक निर्माण को सक्षम करने के लिए पिछली सीमाओं को दूर करता है।
यह शोध पत्र यह स्थापित करता है कि एक गणनीय ऑर्डिनल द्वारा अनुक्रमित फिक्स्ड पॉइंट्स वाले लीनियर लॉजिक के लिए अनंत (infinitary) सु wellfounded प्रणालियों में प्रमाणिकता, हाइपर-अरिथमेटिकल पदानुक्रम के स्तर के लिए पूर्ण है, जो कट एलिमिनेशन (cut elimination) और फोकसिंग (focusing) सहित नए प्रमाण-सिद्धांतिक आधारों के माध्यम से प्राप्त किया गया एक परिणाम है।
यह शोध पत्र सिमेट्रिक पॉलीकैटेगरीज (symmetric polycategories) में एनरिचमेंट (enrichment) और कोटेन्सर्स (cotensors) का उपयोग करके उच्च-क्रम सर्किट सिद्धांतों (higher-order circuit theories) के लिए एक श्रेणीगत ढांचा स्थापित करता है, जो यह प्रदर्शित करता है कि उनके संरचनात्मक नियम उच्च-क्रम क्वांटम सिद्धांत की प्रमुख विशेषताओं को समाहित करते हैं और यह सिद्ध करता है कि ऐसा कोई भी सिद्धांत स्ट्रॉन्ग प्रोफंक्टर्स (strong profunctors) के सिद्धांत में समाहित हो जाता है।
यह शोध पत्र एक प्रोटोटाइप सिस्टम प्रस्तुत करता है जो एक साझा इक्वेशनल हॉर्न फ्रैगमेंट (equational Horn fragment) के माध्यम से प्रूफ़ ऑब्लिगेशन्स (proof obligations) को अनुवादित करके Agda और Vampire ATP के बीच सेतु बनाता है, जिससे उन जटिल गणितीय गुणों के लिए स्वचालित रचनात्मक प्रमाणों (constructive proofs) का निर्माण संभव हो पाता है जिन्हें पहले कई दिनों के मैनुअल प्रयास की आवश्यकता होती थी।
यह शोध पत्र जनरल गेम प्लेइंग परिवेश के भीतर चार लार्ज लैंग्वेज मॉडल्स की औपचारिक तर्क क्षमताओं का मूल्यांकन करता है, जिससे यह पता चलता है कि हालांकि वर्तमान मॉडल्स ने महत्वपूर्ण प्रगति दिखाई है, लेकिन कार्य की जटिलता और स्टेप डेप्थ बढ़ने के साथ उनका प्रदर्शन घट जाता है, जो अक्सर काल्पनिक नियमों (hallucinated rules) और सिंटैक्टिक गलतियों जैसी विशिष्ट तर्क संबंधी त्रुटियों के कारण होता है।
यह शोधपत्र यह प्रदर्शित करता है कि विपरीत सुझाव देने वाली प्रारंभिक अंतर्ज्ञानों के बावजूद, संकुचन (contraction) या विलोपन (weakening) के साथ कम्यूटेटिव फुल लैम्बेक कैलकुलस का प्रत्येक विस्तार, जो एक कट-फ्री हाइपरसीक्वेंट कैलकुलस को स्वीकार करता है, उसका प्रमाणयोग्यता (provability) पर एक इष्टतम एकरमैनियन (Ackermannian) ऊपरी आबंध (upper bound) होता है, जिसे हाइपर-एकरमैनियन स्तरों तक जटिलता की छलांग से बचने के लिए सीक्वेंट्स के बीच नवीन निर्भरताओं का लाभ उठाकर प्राप्त किया गया है।
यह शोध पत्र कमजोर मेमोरी मॉडल्स के तहत समवर्ती कार्यक्रमों (concurrent programs) में लाइवनेस गुणों (liveness properties) के बारे में तर्क करने के लिए पहले प्रूफ़ कैलकुलस (proof calculus) को प्रस्तुत करता है, जो टिकट लॉक एल्गोरिदम (Ticket lock algorithm) के लिए स्टार्वेशन फ्रीडम (starvation freedom) को औपचारिक रूप से सिद्ध करने हेतु मेमोरी फेयरनेस (memory fairness) और कमजोर मेमोरी रैंकिंग फलनों (weak memory ranking functions) के साथ मन्ना और पुनेली (Manna and Pnueli) के रिस्पॉन्स नियमों का विस्तार करता है।
यह शोध पत्र एक हाइब्रिड सत्यापन दृष्टिकोण प्रस्तावित करता है जो संरचनात्मक लूप अनुकूलन, जैसे कि फुल लूप अनरोलिंग, के औपचारिक सत्यापन को सक्षम करने के लिए एक सामान्य एब्स्ट्रैक्ट इंटरफ़ेस के माध्यम से स्मॉल-स्टेप और बिग-स्टेप सिमेंटिक्स को एकीकृत करता है, जिससे कंपसर्ट (CompCert) कंपाइलर पाइपलाइन के भीतर सभी टॉप-लेवल सिमेंटिक गारंटियों को सुरक्षित रखा जा सके।