1088 पेपर
यह शोधपत्र इनक्विज़िटिव फर्स्ट-ऑर्डर मोडल लॉजिक के लिए एक पूर्ण लेबल वाले सीक्वेंट कैलकुलस का परिचय देता है, जो वैश्विक सुपरवेनिएंस (global supervenience) को संभालने के लिए पिछले कार्यों का विस्तार करता है और इसकी स्ट्रॉन्ग कम्प्लीटनेस (strong completeness) के साथ-साथ नियम व्युत्क्रमणीयता (rule invertibility) और कट एडमिसिबिलिटी (cut admissibility) जैसे प्रमुख संरचनात्मक गुणों को सिद्ध करता है।
यह शोध पत्र सहज बोधगम्य (इंट्यूशनिस्टिक) मोनोटोन मोडल लॉजिक IM और इसके विस्तारों के लिए एक सिमेंटिक लक्षण वर्णन और एक संरचित प्रमाण कैलकुलस प्रदान करता है, जो उनकी निर्णयक्षमता (decidability) को स्थापित करता है और मोनोटोन और सामान्य मोडल लॉजिक के रचनात्मक वेरिएंट्स के बीच एक महत्वपूर्ण सादृश्य को रेखांकित करता है।
यह शोध पत्र MPos-हाइपरफॉर्मलिज्म (hyperformalism) को पेश करके प्रासंगिक मोडल लॉजिक्स (modal logics) में हाइपरफॉर्मलिज्म की अवधारणा का विस्तार करता है, यह सिद्ध करता है कि दुर्बल तर्क B-Box इस गुण को रखता है, विशिष्ट गैर-समान प्रतिस्थापन (non-uniform substitutions) के तहत इसकी क्लोजर (closure) की जांच करता है, वेरिएबल शेयरिंग प्रॉपर्टी (variable sharing property) को परिष्कृत करता है, और K-MPos को शास्त्रीय मोडल लॉजिक K के सबसे बड़े MPos-हाइपरफॉर्मल उप-तर्क (sublogic) के रूप में परिभाषित करता है।
यह शोध पत्र कैंटर डेरिवेटिव (Cantor derivative) के साथ संयुक्त एक पाथ-रीचेबिलिटी मोडैलिटी (path-reachability modality) के टोपोलॉजिकल सिमेंटिक्स की जांच करता है, जो T1 टोपोलॉजी और मेट्रिक स्पेस के लिए सुदृढ़ और पूर्ण स्वयंसिद्ध प्रणालियाँ (axiomatic systems) प्रदान करता है, निर्णायकता (decidability) स्थापित करता है, और परिमित मॉडल गुण (finite model property) को सिद्ध करने के लिए एक पड़ोस-समान (neighborhood-like) सिमेंटिक्स प्रस्तुत करता है।
यह शोध पत्र सहज बोधगम्य (इंट्यूशनिस्टिक) मोडल लॉजिक FIK के लिए एक उथले (शैलो) सीक्वेंट कैलकुलस का परिचय देता है, जो इसकी वाक्यात्मक पूर्णता को सिद्ध करता है और इसके निर्णय समस्या (डिसीजन प्रॉब्लम) के लिए एक EXPSPACE ऊपरी सीमा स्थापित करता है, जिससे IK की अनुमानित गैर-तत्वीय (नॉन-एलिमेंट्री) जटिलता की तुलना में काफी कम जटिलता प्रदर्शित होती है।
यह शोध पत्र CEGARBox++ प्रस्तुत करता है, जो एक C++ कार्यान्वयन है जो CEGAR-tableaux में मोडल रेजोल्यूशन (KSP) को SAT-शॉर्टकट्स के रूप में एकीकृत करता है, जो विशेष रूप से बड़े सैटिस्फिएबल मोडल समस्याओं पर स्टैंडअलोन KSP और RECAR-उन्नत CEGAR-tableaux दोनों की तुलना में बेहतर प्रदर्शन प्रदर्शित करता है।
यह शोध पत्र यह स्थापित करता है कि सहजतावादी मोडल लॉजिक (intuitionistic modal logic) IK, IK-बिसिम्यूलेशन (IK-bisimulation) को परिभाषित करके, हेनेसी-मिलनर-शैली (Hennessy-Milner-style) का अभिलक्षण सिद्ध करके, और लूस के प्रमेय (Łoś's Theorem) एवं गणनीय संतृप्ति (countable saturation) जैसे सहजतावादी समकक्षों सहित संगत मॉडल-सैद्धांतिक उपकरणों को विकसित करके, सहजतावादी प्रथम-क्रम तर्क (intuitionistic first-order logic) का सटीक बिसिम्यूलेशन-अपरिवर्तनीय खंड (bisimulation-invariant fragment) है।
यह शोध पत्र -संयोजित मीट्रिक स्थानों (दूरी मोडैलिटीज़ और यूनिवर्सल मोडैलिटी का उपयोग करते हुए) और शास्त्रीय रूप से संयोजित मीट्रिक स्थानों (टोपोलॉजिकल, यूनिवर्सल और एक एकल दूरी मोडैलिटी का उपयोग करते हुए) के मोडल लॉजिक्स के लिए पूर्ण स्वयंसिद्धीकरण प्रदान करता है और परिमित मॉडल गुण को सिद्ध करता है।
यह शोध पत्र स्तरीकृत तर्क प्रणालियों SCP और SCP1 को प्रस्तुत करता है, जो शून्य प्रतिसंभाव्य सत्यों (vacuous counterpossible truths) से बचने के लिए तार्किक और आध्यात्मिक असंभवता के बीच अंतर करते हैं और साथ ही उनकी सुदृढ़ता, पूर्णता और निर्णयक्षमता को सिद्ध करते हैं।
यह शोध पत्र ऋणात्मक रूप से संकेतित (negatively pointed) मोडल एबेलियन एल-ग्रुप्स की विविधता को प्रस्तुत करके और एक आर्कमिडियन-शैली के नियम के माध्यम से परिमित अभिलेखन (finitary axiomatizations) की सीमाओं को संबोधित करते हुए, वास्तविक संख्याओं पर संकेतित मोडल एबेलियन तर्क के लिए एक संबंधात्मक अर्थविज्ञान और एक अनंत बीजगणितीय पूर्णता परिणाम स्थापित करता है।