टेम्पोरल लॉजिक: Difference between revisions

From Vigyanwiki
No edit summary
 
(21 intermediate revisions by 8 users not shown)
Line 1: Line 1:
[[तर्क]] में, लौकिक तर्क [[समय]] के संदर्भ में योग्य प्रस्तावों का प्रतिनिधित्व करने और उनके बारे में तर्क करने के लिए नियमों और प्रतीकों की कोई भी प्रणाली है (उदाहरण के लिए, मैं ''प्रायः'' भूखा हूं, मैं ''आखिरकार'' भूखा रहूंगा, या मैं भूखा रहूँगा ''जब तक'' मैं कुछ खा लूँगा )। यह कभी-कभी तनावपूर्ण तर्क को संदर्भित करने के लिए भी प्रयोग किया जाता है, 1 9 50 के दशक के अंत में [[आर्थर प्रायर]] द्वारा शुरू की गई लौकिक तर्क की एक [[मॉडल तर्क]]-आधारित प्रणाली, [[उनका संघर्ष]] द्वारा महत्वपूर्ण योगदान के साथ। इसे [[कंप्यूटर वैज्ञानिकों]], विशेष रूप से [[आमिर पनुएली]] और तर्कशास्त्रियों द्वारा विकसित किया गया है।
[[तर्क|लॉजिक]] में, '''टेम्पोरल लॉजिक''' [[समय]] के संदर्भ में योग्य प्रस्तावों का प्रतिनिधित्व करने और उनके बारे में लॉजिक करने के लिए नियमों और प्रतीकों की कोई भी प्रणाली है (उदाहरण के लिए, मैं ''प्रायः'' भूखा हूं, मैं ''आखिरकार'' भूखा रहूंगा, या मैं भूखा रहूँगा ''जब तक'' मैं कुछ खा लूँगा )। यह कभी-कभी तनावपूर्ण लॉजिक को संदर्भित करने के लिए भी प्रयोग किया जाता है, 1950 के दशक के अंत में [[आर्थर प्रायर]] द्वारा प्रांरम्भ की गई टेम्पोरल लॉजिक की एक [[मॉडल तर्क|मॉडल लॉजिक]]-आधारित प्रणाली, [[उनका संघर्ष]] द्वारा महत्वपूर्ण योगदान के साथ। इसे [[कंप्यूटर वैज्ञानिकों]], विशेष रूप से [[आमिर पनुएली]] और लॉजिकशास्त्रियों द्वारा विकसित किया गया है।


टेम्पोरल लॉजिक को [[औपचारिक सत्यापन]] में एक महत्वपूर्ण अनुप्रयोग मिला है, जहां इसका उपयोग हार्डवेयर या सॉफ्टवेयर सिस्टम की आवश्यकताओं को बताने के लिए किया जाता है। उदाहरण के लिए, कोई यह कहना चाह सकता है कि ''जब भी'' एक अनुरोध किया जाता है, संसाधन तक पहुंच ''आखिरकार'' दी जाती है, लेकिन यह दो अनुरोधकर्ताओं को एक साथ ''कभी नहीं'' दी जाती है। इस तरह के बयान को अस्थायी तर्क में आसानी से व्यक्त किया जा सकता है।
टेम्पोरल लॉजिक को [[औपचारिक सत्यापन]] में एक महत्वपूर्ण अनुप्रयोग मिला है, जहां इसका उपयोग हार्डवेयर या सॉफ्टवेयर सिस्टम की आवश्यकताओं को बताने के लिए किया जाता है। उदाहरण के लिए, कोई यह कहना चाह सकता है कि ''जब भी'' एक अनुरोध किया जाता है, संसाधन तक पहुंच ''आखिरकार'' दी जाती है, लेकिन यह दो अनुरोधकर्ताओं को एक साथ ''कभी नहीं'' दी जाती है। इस तरह के बयान को अस्थायी लॉजिक में आसानी से व्यक्त किया जा सकता है।


== प्रेरणा ==
== प्रेरणा ==
कथन पर विचार करें मुझे भूख लगी है। हालांकि इसका अर्थ समय में स्थिर है, कथन का सत्य मूल्य समय में भिन्न हो सकता है। कभी यह सच होता है, और कभी झूठ, लेकिन कभी भी सच और झूठ एक साथ नहीं। एक लौकिक तर्क में, एक बयान में एक सत्य मूल्य हो सकता है जो समय के साथ बदलता रहता है - एक अस्थायी तर्क के विपरीत, जो केवल उन बयानों पर लागू होता है जिनके सत्य मूल्य समय में स्थिर होते हैं। समय के साथ सत्य-मूल्य का यह उपचार लौकिक तर्क को [[कम्प्यूटेशनल क्रिया तर्क]] से अलग करता है।
कथन पर विचार करें मुझे भूख लगी है। हालांकि इसका अर्थ समय में स्थिर है, कथन का सत्य मूल्य समय में भिन्न हो सकता है। कभी यह सच होता है, और कभी झूठ, लेकिन कभी भी सच और झूठ एक साथ नहीं। एक टेम्पोरल लॉजिक में, एक बयान में एक सत्य मूल्य हो सकता है जो समय के साथ बदलता रहता है - एक अस्थायी लॉजिक के विपरीत, जो केवल उन बयानों पर लागू होता है जिनके सत्य मूल्य समय में स्थिर होते हैं। समय के साथ सत्य-मूल्य का यह उपचार टेम्पोरल लॉजिक को [[कम्प्यूटेशनल क्रिया तर्क|कम्प्यूटेशनल क्रिया लॉजिक]] से अलग करता है।


टेम्पोरल लॉजिक में प्रायः टाइमलाइन के बारे में तर्क करने की क्षमता होती है। तथाकथित रैखिक-समय तर्क इस प्रकार के तर्क तक ही सीमित हैं। ब्रांचिंग-टाइम लॉजिक्स, हालांकि, कई समयसीमाओं के बारे में तर्क कर सकते हैं। यह उन वातावरणों के विशेष उपचार की अनुमति देता है जो अप्रत्याशित रूप से कार्य कर सकते हैं।
टेम्पोरल लॉजिक में प्रायः टाइमलाइन के बारे में लॉजिक करने की क्षमता होती है। तथाकथित रैखिक-समय लॉजिक इस प्रकार के लॉजिक तक ही सीमित हैं। ब्रांचिंग-टाइम लॉजिक्स, हालांकि, कई समयसीमाओं के बारे में लॉजिक कर सकते हैं। यह उन वातावरणों के विशेष उपचार की अनुमति देता है जो अप्रत्याशित रूप से कार्य कर सकते हैं।
उदाहरण को जारी रखने के लिए, ब्रांचिंग-टाइम लॉजिक में हम कह सकते हैं कि एक संभावना है कि मैं प्रायः के लिए भूखा रहूँगा, और एक संभावना है कि अंततः मुझे भूख नहीं लगेगी। यदि हम नहीं जानते कि मुझे कभी खिलाया जाएगा या नहीं, तो ये दोनों कथन सत्य हो सकते हैं।
उदाहरण को जारी रखने के लिए, ब्रांचिंग-टाइम लॉजिक में हम कह सकते हैं कि एक संभावना है कि मैं प्रायः के लिए भूखा रहूँगा, और एक संभावना है कि अंततः मुझे भूख नहीं लगेगी। यदि हम नहीं जानते कि मुझे कभी खिलाया जाएगा या नहीं, तो ये दोनों कथन सत्य हो सकते हैं।


== इतिहास ==
== इतिहास ==
हालांकि [[अरस्तू]] का तर्क लगभग पूरी तरह से स्पष्ट न्यायवाक्य के सिद्धांत से संबंधित है, उनके काम में ऐसे अंश हैं जिन्हें अब लौकिक तर्क की प्रत्याशा के रूप में देखा जाता है, और प्रथम-क्रम तर्क का एक प्रारंभिक, आंशिक रूप से विकसित रूप हो सकता है। मोडल [[द्विसंयोजक तर्क]] तर्क। अरस्तू विशेष रूप से भविष्य की आकस्मिकताओं की समस्या से चिंतित था, जहां वह यह स्वीकार नहीं कर सकता था कि भविष्य की घटनाओं के बारे में बयानों पर द्वंद्व का सिद्धांत लागू होता है, यानी हम वर्तमान में यह तय कर सकते हैं कि भविष्य की घटनाओं के बारे में कोई बयान सही है या गलत, जैसे कि कल एक समुद्री युद्ध हो।<ref>Vardi 2008, p. 153</ref>
हालांकि [[अरस्तू]] का लॉजिक लगभग पूरी तरह से स्पष्ट न्यायवाक्य के सिद्धांत से संबंधित है, उनके काम में ऐसे अंश हैं जिन्हें अब टेम्पोरल लॉजिक की प्रत्याशा के रूप में देखा जाता है, और प्रथम-क्रम लॉजिक का एक प्रारंभिक, आंशिक रूप से विकसित रूप हो सकता है। मोडल [[द्विसंयोजक तर्क|द्विसंयोजक लॉजिक]] लॉजिक। अरस्तू विशेष रूप से भविष्य की आकस्मिकताओं की समस्या से चिंतित था, जहां वह यह स्वीकार नहीं कर सकता था कि भविष्य की घटनाओं के बारे में बयानों पर द्वंद्व का सिद्धांत लागू होता है, यानी हम वर्तमान में यह तय कर सकते हैं कि भविष्य की घटनाओं के बारे में कोई बयान सही है या गलत, जैसे कि कल एक समुद्री युद्ध हो।<ref>Vardi 2008, p. 153</ref>
सहस्राब्दी के लिए बहुत कम विकास हुआ, [[चार्ल्स सैंडर्स पियर्स]] ने 19 वीं शताब्दी में उल्लेख किया:<ref name=v154>Vardi 2008, p. 154</ref>
सहस्राब्दी के लिए बहुत कम विकास हुआ, [[चार्ल्स सैंडर्स पियर्स]] ने 19 वीं शताब्दी में उल्लेख किया:<ref name=v154>Vardi 2008, p. 154</ref>
{{cquote|समय को आमतौर पर तर्कशास्त्रियों द्वारा 'एक्स्ट्रालॉजिकल' पदार्थ कहा जाता है। मैंने कभी इस राय को साझा नहीं किया। लेकिन मैंने सोचा है कि तर्क अभी तक विकास की स्थिति तक नहीं पहुंचा था, जिस पर इसके रूपों के लौकिक संशोधनों की शुरूआत से बड़ी गड़बड़ी नहीं होगी; और मैं अभी भी उस तरह की सोच का हूं।}}
{{cquote|समय को सामान्यतः तर्कशास्त्रियों द्वारा 'एक्स्ट्रालॉजिकल' पदार्थ कहा जाता है। मैंने कभी इस राय को साझा नहीं किया। लेकिन मैंने सोचा है कि तर्क अभी तक विकास की स्थिति तक नहीं पहुंचा था, जिस पर इसके रूपों के लौकिक संशोधनों की प्रांरम्भ से बड़ी गड़बड़ी नहीं होगी; और मैं अभी भी उस तरह की सोच का हूं।}}


आश्चर्यजनक रूप से चार्ल्स सैंडर्स पियर्स के लिए, लौकिक तर्क की पहली प्रणाली का निर्माण किया गया था, जहाँ तक हम जानते हैं, 20 वीं शताब्दी के पहले भाग में। हालांकि आर्थर प्रायर को व्यापक रूप से टेम्पोरल लॉजिक के संस्थापक के रूप में जाना जाता है, इस तरह के लॉजिक की पहली औपचारिकता 1947 में पोलिश तर्कशास्त्री जेरज़ी लोस द्वारा प्रदान की गई थी।<ref name=":0">{{Cite book|last=Łoś|first=Jerzy (1920-1998)|url=http://dlibra.umcs.lublin.pl/dlibra/doccontent?id=4085|title=Podstawy analizy metodologicznej kanonów Milla|last2=Łoś|first2=Jerzy (1920-1998)|date=1947|publisher=nakł. Uniwersytetu Marii Curie-Skłodowskiej}}</ref> अपने काम पोडस्टावी एनालिज़ी मेटोडोलॉजिक्ज़नेज कानोनोव मिल्ला (द फाउंडेशन ऑफ़ ए मेथोडोलॉजिकल एनालिसिस ऑफ़ मिल्स मेथड्स) में उन्होंने मिल के सिद्धांतों का एक औपचारिक रूप प्रस्तुत किया। जेरज़ी लॉस के दृष्टिकोण में, समय कारक पर जोर दिया गया था। इस प्रकार, अपने लक्ष्य तक पहुँचने के लिए, उसे एक तर्क का निर्माण करना पड़ा जो लौकिक कार्यों की औपचारिकता के लिए साधन प्रदान कर सके। तर्क को जेरज़ी लॉस के मुख्य उद्देश्य के प्रतिफल के रूप में देखा जा सकता है,<ref name=":1">{{Cite journal|last=Øhrstrøm|first=Peter|date=2019|title=The Significance of the Contributions of A.N.Prior and Jerzy Łoś in the Early History of Modern Temporal Logic|url=https://vbn.aau.dk/en/publications/the-significance-of-the-contributions-of-anprior-and-jerzy-%C5%82o%C5%9B-in|journal=Logic and Philosophy of Time: Further Themes from Prior, Volume 2|language=English}}</ref> यद्यपि यह पहला स्थितीय तर्क था, जिसे एक रूपरेखा के रूप में, बाद में ज्ञानशास्त्रीय तर्क में जेरज़ी लॉस के आविष्कारों के लिए इस्तेमाल किया गया था। लॉजिक में सिंटैक्स प्रायर के टेंस लॉजिक से बहुत अलग है, जो मोडल ऑपरेटरों का उपयोग करता है। जेरज़ी लॉस  'लॉजिक की भाषा बल्कि एक अहसास ऑपरेटर का उपयोग करती है, जो स्थिति संबंधी तर्क के लिए विशिष्ट है, जो विशिष्ट संदर्भ के साथ अभिव्यक्ति को बांधता है जिसमें इसका सत्य-मूल्य माना जाता है। जेरज़ी लॉस के कार्य में यह माना गया संदर्भ केवल लौकिक था, इस प्रकार अभिव्यक्ति विशिष्ट क्षणों या समय के अंतराल से बंधी हुई थी।
आश्चर्यजनक रूप से चार्ल्स सैंडर्स पियर्स के लिए, टेम्पोरल लॉजिक की पहली प्रणाली का निर्माण किया गया था, जहाँ तक हम जानते हैं, 20 वीं शताब्दी के पहले भाग में। हालांकि आर्थर प्रायर को व्यापक रूप से टेम्पोरल लॉजिक के संस्थापक के रूप में जाना जाता है, इस तरह के लॉजिक की पहली औपचारिकता 1947 में पोलिश लॉजिकशास्त्री जेरज़ी लोस द्वारा प्रदान की गई थी।<ref name=":0">{{Cite book|last=Łoś|first=Jerzy (1920-1998)|url=http://dlibra.umcs.lublin.pl/dlibra/doccontent?id=4085|title=Podstawy analizy metodologicznej kanonów Milla|last2=Łoś|first2=Jerzy (1920-1998)|date=1947|publisher=nakł. Uniwersytetu Marii Curie-Skłodowskiej}}</ref> अपने काम पोडस्टावी एनालिज़ी मेटोडोलॉजिक्ज़नेज कानोनोव मिल्ला (द फाउंडेशन ऑफ़ ए मेथोडोलॉजिकल एनालिसिस ऑफ़ मिल्स मेथड्स) में उन्होंने मिल के सिद्धांतों का एक औपचारिक रूप प्रस्तुत किया। जेरज़ी लॉस के दृष्टिकोण में, समय कारक पर जोर दिया गया था। इस प्रकार, अपने लक्ष्य तक पहुँचने के लिए, उसे एक लॉजिक का निर्माण करना पड़ा जो लौकिक कार्यों की औपचारिकता के लिए साधन प्रदान कर सके। लॉजिक को जेरज़ी लॉस के मुख्य उद्देश्य के प्रतिफल के रूप में देखा जा सकता है,<ref name=":1">{{Cite journal|last=Øhrstrøm|first=Peter|date=2019|title=The Significance of the Contributions of A.N.Prior and Jerzy Łoś in the Early History of Modern Temporal Logic|url=https://vbn.aau.dk/en/publications/the-significance-of-the-contributions-of-anprior-and-jerzy-%C5%82o%C5%9B-in|journal=Logic and Philosophy of Time: Further Themes from Prior, Volume 2|language=English}}</ref> यद्यपि यह पहला स्थितीय लॉजिक था, जिसे एक रूपरेखा के रूप में, बाद में ज्ञानशास्त्रीय लॉजिक में जेरज़ी लॉस के आविष्कारों के लिए इस्तेमाल किया गया था। लॉजिक में सिंटैक्स प्रायर के टेंस लॉजिक से बहुत अलग है, जो मोडल ऑपरेटरों का उपयोग करता है। जेरज़ी लॉस  'लॉजिक की भाषा बल्कि एक अहसास ऑपरेटर का उपयोग करती है, जो स्थिति संबंधी लॉजिक के लिए विशिष्ट है, जो विशिष्ट संदर्भ के साथ अभिव्यक्ति को बांधता है जिसमें इसका सत्य-मूल्य माना जाता है। जेरज़ी लॉस के कार्य में यह माना गया संदर्भ केवल लौकिक था, इस प्रकार अभिव्यक्ति विशिष्ट क्षणों या समय के अंतराल से बंधी हुई थी।


बाद के वर्षों में, आर्थर प्रायर द्वारा लौकिक तर्कशास्त्र का शोध शुरू हुआ।<ref name=":1" />वह स्वतंत्र इच्छा और [[पूर्वनियति]] के दार्शनिक निहितार्थों से चिंतित थे। उनकी पत्नी के अनुसार, उन्होंने पहली बार 1953 में लौकिक तर्क को औपचारिक बनाने पर विचार किया। उनके शोध के परिणाम पहली बार 1954 में [[ वेलिंग्टन ]] में सम्मेलन में प्रस्तुत किए गए।<ref name=":1" />पहले प्रस्तुत की गई प्रणाली वाक्य रचना की दृष्टि से जेरज़ी लॉस तर्क के समान थी, हालांकि 1955 तक उन्होंने प्रायर के औपचारिक तर्क में परिशिष्ट 1 के अंतिम खंड में स्पष्ट रूप से जेरज़ी लॉस के कार्य का उल्लेख नहीं किया था।<ref name=":1" />
बाद के वर्षों में, आर्थर प्रायर द्वारा टेम्पोरल लॉजिकशास्त्र का शोध प्रांरम्भ हुआ।<ref name=":1" />वह स्वतंत्र इच्छा और [[पूर्वनियति]] के दार्शनिक निहितार्थों से चिंतित थे। उनकी पत्नी के अनुसार, उन्होंने पहली बार 1953 में टेम्पोरल लॉजिक को औपचारिक बनाने पर विचार किया। उनके शोध के परिणाम पहली बार 1954 में [[ वेलिंग्टन ]] में सम्मेलन में प्रस्तुत किए गए।<ref name=":1" />पहले प्रस्तुत की गई प्रणाली वाक्य रचना की दृष्टि से जेरज़ी लॉस लॉजिक के समान थी, हालांकि 1955 तक उन्होंने प्रायर के औपचारिक लॉजिक में परिशिष्ट 1 के अंतिम खंड में स्पष्ट रूप से जेरज़ी लॉस के कार्य का उल्लेख नहीं किया था।<ref name=":1" />


आर्थर प्रायर ने 1955-6 में [[ऑक्सफोर्ड विश्वविद्यालय]] में इस विषय पर व्याख्यान दिया, और 1957 में एक पुस्तक, टाइम एंड मॉडेलिटी प्रकाशित की, जिसमें उन्होंने दो लौकिक संयोजकों ([[मोडल ऑपरेटर|मोडल]] ऑपरेटर्स ), एफ और पी के साथ एक प्रस्तावपरक तर्क मोडल लॉजिक पेश किया। भविष्य में कुछ समय और अतीत में कुछ समय के अनुरूप। इस प्रारंभिक कार्य में प्रायर ने समय को रेखीय माना। हालाँकि, 1958 में, उन्हें शाऊल क्रिपके का एक पत्र मिला, जिसने बताया कि यह धारणा शायद अनुचित है। एक ऐसे विकास में जिसने कंप्यूटर विज्ञान में इसी तरह के एक को पूर्वाभास दिया, प्रायर ने इसे सलाह के तहत लिया, और ब्रांचिंग टाइम के दो सिद्धांतों को विकसित किया, जिसे उन्होंने ओखमिस्ट और पीयरसियन कहा।<ref name="v154" />, 1958 और 1965 के बीच प्रायर ने [[चार्ल्स लियोनार्ड हैम्बलिन]] के साथ भी पत्राचार किया था, और इस क्षेत्र में कई शुरुआती विकासों को इस पत्राचार से खोजा जा सकता है, उदाहरण के लिए हैम्ब्लिन निहितार्थ। प्रायर ने 1967 में इस विषय पर अपना सबसे परिपक्व काम पास्ट, प्रेजेंट, एंड फ्यूचर प्रकाशित किया। दो साल बाद उनकी मृत्यु हो गई।<ref>{{cite book|author1=Peter Øhrstrøm|author2=Per F. V. Hasle|title=Temporal logic: from ancient ideas to artificial intelligence|year=1995|publisher=Springer|isbn=978-0-7923-3586-3}} pp.&nbsp;176–178, 210</ref>
आर्थर प्रायर ने 1955-6 में [[ऑक्सफोर्ड विश्वविद्यालय]] में इस विषय पर व्याख्यान दिया, और 1957 में एक पुस्तक, टाइम एंड मॉडेलिटी प्रकाशित की, जिसमें उन्होंने दो लौकिक संयोजकों ([[मोडल ऑपरेटर|मोडल]] ऑपरेटर्स ), एफ और पी के साथ एक प्रस्तावपरक लॉजिक मोडल लॉजिक पेश किया। भविष्य में कुछ समय और अतीत में कुछ समय के अनुरूप। इस प्रारंभिक कार्य में प्रायर ने समय को रेखीय माना। हालाँकि, 1958 में, उन्हें शाऊल क्रिपके का एक पत्र मिला, जिसने बताया कि यह धारणा शायद अनुचित है। एक ऐसे विकास में जिसने कंप्यूटर विज्ञान में इसी तरह के एक को पूर्वाभास दिया, प्रायर ने इसे सलाह के तहत लिया, और ब्रांचिंग टाइम के दो सिद्धांतों को विकसित किया, जिसे उन्होंने ओखमिस्ट और पीयरसियन कहा।<ref name="v154" />, 1958 और 1965 के बीच प्रायर ने [[चार्ल्स लियोनार्ड हैम्बलिन]] के साथ भी पत्राचार किया था, और इस क्षेत्र में कई शुरुआती विकासों को इस पत्राचार से खोजा जा सकता है, उदाहरण के लिए हैम्ब्लिन निहितार्थ। प्रायर ने 1967 में इस विषय पर अपना सबसे परिपक्व काम पास्ट, प्रेजेंट, एंड फ्यूचर प्रकाशित किया। दो साल बाद उनकी मृत्यु हो गई।<ref>{{cite book|author1=Peter Øhrstrøm|author2=Per F. V. Hasle|title=Temporal logic: from ancient ideas to artificial intelligence|year=1995|publisher=Springer|isbn=978-0-7923-3586-3}} pp.&nbsp;176–178, 210</ref>
तनावपूर्ण तर्क के साथ, आर्थर प्रायर ने स्थितीय तर्क की कुछ प्रणालियों का निर्माण किया, जो उनके मुख्य विचारों को जेर्जी लोश से विरासत में मिला।<ref name=":2">{{Cite journal|last=Rescher|first=Nicholas|last2=Garson|first2=James|date=January 1969|title=टोपोलॉजिकल लॉजिक|url=https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/topological-logic/5ADE3A9CA7CE00FBD8D69E4DDA8B1BC8|journal=The Journal of Symbolic Logic|language=en|volume=33|issue=4|pages=537–548|doi=10.2307/2271360|issn=0022-4812}}</ref> 60 और 70 के दशक में [[निकोलस रेसचर]] द्वारा स्थितीय लौकिक लॉजिक्स में काम जारी रखा गया था। कालानुक्रमिक तर्क पर नोट (1966), कालानुक्रमिक प्रस्तावों के तर्क पर (1968), स्थलीय तर्क (1968), और टेम्पोरल तर्क (1971) जैसे कार्यों में उन्होंने जेरज़ी लॉस और आर्थर प्रायर की प्रणालियों के बीच संबंधों पर शोध किया। इसके अलावा उन्होंने साबित किया कि आर्थर प्रायर के काल संचालकों को विशिष्ट स्थितीय तर्कशास्त्र में एक अहसास संचालक का उपयोग करके परिभाषित किया जा सकता है।<ref name=":2" />निकोलस रेसचर ने अपने काम में, स्थितीय तर्कशास्त्र की अधिक सामान्य प्रणालियाँ भी बनाईं। हालांकि पहले वाले विशुद्ध रूप से लौकिक उपयोगों के लिए बनाए गए थे, उन्होंने तर्कशास्त्र के लिए टोपोलॉजिकल लॉजिक्स शब्द का प्रस्ताव दिया था, जो एक अहसास ऑपरेटर को सम्मिलित करने के लिए था, लेकिन कोई विशिष्ट लौकिक स्वयंसिद्ध नहीं था - जैसे घड़ी का स्वयंसिद्ध।
तनावपूर्ण लॉजिक के साथ, आर्थर प्रायर ने स्थितीय लॉजिक की कुछ प्रणालियों का निर्माण किया, जो उनके मुख्य विचारों को जेर्जी लोश से विरासत में मिला।<ref name=":2">{{Cite journal|last=Rescher|first=Nicholas|last2=Garson|first2=James|date=January 1969|title=टोपोलॉजिकल लॉजिक|url=https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/topological-logic/5ADE3A9CA7CE00FBD8D69E4DDA8B1BC8|journal=The Journal of Symbolic Logic|language=en|volume=33|issue=4|pages=537–548|doi=10.2307/2271360|issn=0022-4812}}</ref> 60 और 70 के दशक में [[निकोलस रेसचर]] द्वारा स्थितीय लौकिक लॉजिक्स में काम जारी रखा गया था। कालानुक्रमिक लॉजिक पर नोट (1966), कालानुक्रमिक प्रस्तावों के लॉजिक पर (1968), स्थलीय लॉजिक (1968), और टेम्पोरल लॉजिक (1971) जैसे कार्यों में उन्होंने जेरज़ी लॉस और आर्थर प्रायर की प्रणालियों के बीच संबंधों पर शोध किया। इसके अलावा उन्होंने साबित किया कि आर्थर प्रायर के काल संचालकों को विशिष्ट स्थितीय लॉजिकशास्त्र में एक अहसास संचालक का उपयोग करके परिभाषित किया जा सकता है।<ref name=":2" />निकोलस रेसचर ने अपने काम में, स्थितीय लॉजिकशास्त्र की अधिक सामान्य प्रणालियाँ भी बनाईं। हालांकि पहले वाले विशुद्ध रूप से लौकिक उपयोगों के लिए बनाए गए थे, उन्होंने लॉजिकशास्त्र के लिए टोपोलॉजिकल लॉजिक्स शब्द का प्रस्ताव दिया था, जो एक अहसास ऑपरेटर को सम्मिलित करने के लिए था, लेकिन कोई विशिष्ट लौकिक स्वयंसिद्ध नहीं था - जैसे घड़ी का स्वयंसिद्ध।


बाइनरी टेम्पोरल ऑपरेटर ''से'' और ''जब तक'' हंस काम्प द्वारा 1968 में अपनी पीएच.डी. में पेश किए गए थे। थीसिस,<ref>{{cite web|url=https://plato.stanford.edu/entries/logic-temporal/#AddSinUnt |title=टेम्पोरल लॉजिक (स्टैनफोर्ड एनसाइक्लोपीडिया ऑफ फिलॉसफी)|publisher=Plato.stanford.edu |access-date=2014-07-30}}</ref> जिसमें एक महत्वपूर्ण परिणाम भी सम्मिलित है जो लौकिक तर्क को पहले क्रम के तर्क से संबंधित करता है - एक परिणाम जिसे अब काम्प के प्रमेय के रूप में जाना जाता है।<ref name="CarnielliPizzi2008">{{cite book|author1=Walter Carnielli|author2=Claudio Pizzi|title=तौर-तरीके और बहुविधता|url=https://books.google.com/books?id=XpAFM04G6BAC&pg=PA181|year=2008|publisher=Springer|isbn=978-1-4020-8589-5|page=181}}</ref><ref name=v154>Vardi 2008, p. 154</ref><ref name="TessarisFranconi2009">{{cite book|author1=Sergio Tessaris|author2=Enrico Franconi|author3=Thomas Eiter|title=Reasoning Web. Semantic Technologies for Information Systems: 5th International Summer School 2009, Brixen-Bressanone, Italy, August 30 – September 4, 2009, Tutorial Lectures|url=https://books.google.com/books?id=JdyeU7zs4-AC&pg=PA112|year=2009|publisher=Springer|isbn=978-3-642-03753-5|page=112}}</ref>
बाइनरी टेम्पोरल ऑपरेटर ''से'' और ''जब तक'' हंस काम्प द्वारा 1968 में अपनी पीएच.डी. में पेश किए गए थे। थीसिस,<ref>{{cite web|url=https://plato.stanford.edu/entries/logic-temporal/#AddSinUnt |title=टेम्पोरल लॉजिक (स्टैनफोर्ड एनसाइक्लोपीडिया ऑफ फिलॉसफी)|publisher=Plato.stanford.edu |access-date=2014-07-30}}</ref> जिसमें एक महत्वपूर्ण परिणाम भी सम्मिलित है जो टेम्पोरल लॉजिक को पहले क्रम के लॉजिक से संबंधित करता है - एक परिणाम जिसे अब काम्प के प्रमेय के रूप में जाना जाता है।<ref name="CarnielliPizzi2008">{{cite book|author1=Walter Carnielli|author2=Claudio Pizzi|title=तौर-तरीके और बहुविधता|url=https://books.google.com/books?id=XpAFM04G6BAC&pg=PA181|year=2008|publisher=Springer|isbn=978-1-4020-8589-5|page=181}}</ref><ref name=v154>Vardi 2008, p. 154</ref><ref name="TessarisFranconi2009">{{cite book|author1=Sergio Tessaris|author2=Enrico Franconi|author3=Thomas Eiter|title=Reasoning Web. Semantic Technologies for Information Systems: 5th International Summer School 2009, Brixen-Bressanone, Italy, August 30 – September 4, 2009, Tutorial Lectures|url=https://books.google.com/books?id=JdyeU7zs4-AC&pg=PA112|year=2009|publisher=Springer|isbn=978-3-642-03753-5|page=112}}</ref>
औपचारिक सत्यापन में दो प्रारंभिक दावेदार [[रैखिक लौकिक तर्क]] थे, आमिर पनुएली द्वारा एक रैखिक-समय तर्क, और [[ गणना वृक्ष तर्क ]] (सीएलटी), [[मोर्दचाई बेन-अरी]], [[ जौहर मन्ना ]] और अमीर पनुएली द्वारा एक शाखा-समय तर्क। लगभग उसी समय एडमंड एम. क्लार्क|ई द्वारा सीटीएल के लगभग समकक्ष औपचारिकता का सुझाव दिया गया था। एम. क्लार्क और ई. एलन एमर्सन|ई. ए एमर्सन। तथ्य यह है कि दूसरा तर्क पहले की तुलना में [[निर्णय समस्या]] कम्प्यूटेशनल जटिलता हो सकता है, सामान्य तौर पर ब्रांचिंग- और रैखिक-समय के तर्कों पर प्रतिबिंबित नहीं होता है, जैसा कि कभी-कभी तर्क दिया गया है। बदले में, इमर्सन और लेई दिखाते हैं कि किसी भी रैखिक-समय तर्क को शाखा-समय तर्क तक बढ़ाया जा सकता है जिसे उसी जटिलता से तय किया जा सकता है।
औपचारिक सत्यापन में दो प्रारंभिक दावेदार [[रैखिक लौकिक तर्क|रैखिक टेम्पोरल लॉजिक]] थे, आमिर पनुएली द्वारा एक रैखिक-समय लॉजिक, और [[ गणना वृक्ष तर्क | गणना वृक्ष लॉजिक]] (सीएलटी), [[मोर्दचाई बेन-अरी]], [[ जौहर मन्ना ]] और अमीर पनुएली द्वारा एक शाखा-समय लॉजिक। लगभग उसी समय एडमंड एम. क्लार्क|ई द्वारा सीटीएल के लगभग समकक्ष औपचारिकता का सुझाव दिया गया था। एम. क्लार्क और ई. एलन एमर्सन|ई. ए एमर्सन। तथ्य यह है कि दूसरा लॉजिक पहले की तुलना में [[निर्णय समस्या]] कम्प्यूटेशनल जटिलता हो सकता है, सामान्य तौर पर ब्रांचिंग- और रैखिक-समय के लॉजिकों पर प्रतिबिंबित नहीं होता है, जैसा कि कभी-कभी लॉजिक दिया गया है। बदले में, इमर्सन और लेई दिखाते हैं कि किसी भी रैखिक-समय लॉजिक को शाखा-समय लॉजिक तक बढ़ाया जा सकता है जिसे उसी जटिलता से तय किया जा सकता है।


== मूस 'स्थितीय तर्क ==
== लॉस 'स्थितीय लॉजिक ==
जेरज़ी लॉस लॉजिक को उनके 1947 के मास्टर की थीसिस द फ़ाउंडेशन ऑफ़ ए मेथोडोलॉजिकल एनालिसिस ऑफ़ मिल्स मेथड्स के रूप में प्रकाशित किया गया था।<ref name= Tkaczyk 2019 259–276>{{Cite journal|last=Tkaczyk|first=Marcin|last2=Jarmużek|first2=Tomasz|date=2019|title=जेरज़ी लोश पोजिशनल कैलकुलस एंड द ओरिजिन ऑफ़ टेम्पोरल लॉजिक|url=https://apcz.umk.pl/LLP/article/view/LLP.2018.013|journal=Logic and Logical Philosophy|language=en|volume=28|issue=2|pages=259–276|doi=10.12775/LLP.2018.013|issn=2300-9802|doi-access=free}</ref> उनकी दार्शनिक और औपचारिक अवधारणाओं को लविव-वारसॉ स्कूल ऑफ़ लॉजिक की निरंतरता के रूप में देखा जा सकता है, क्योंकि उनके पर्यवेक्षक जेरज़ी स्लूपेकी थे, जो जन लुकासिविक्ज़ के शिष्य थे। पेपर का 1977 तक अंग्रेजी में अनुवाद नहीं किया गया था, हालांकि हेनरिक हाईज़ ने 1951 में एक संक्षिप्त, लेकिन सूचनात्मक, [[प्रतीकात्मक तर्क का जर्नल]] में समीक्षा प्रस्तुत की। इस समीक्षा में जेरज़ी लॉस के काम की मूल अवधारणाएँ सम्मिलित थीं और तार्किक समुदाय के बीच उनके परिणामों को लोकप्रिय बनाने के लिए पर्याप्त थीं। इस कार्य का मुख्य उद्देश्य मिल के सिद्धांतों को औपचारिक तर्क के ढांचे में प्रस्तुत करना था। इस लक्ष्य को प्राप्त करने के लिए लेखक ने मिल की अवधारणा की संरचना में लौकिक कार्यों के महत्व पर शोध किया। ऐसा करने के बाद, उन्होंने तर्क की अपनी स्वयंसिद्ध प्रणाली प्रदान की जो मिल के सिद्धांतों के साथ-साथ उनके लौकिक पहलुओं के लिए एक रूपरेखा के रूप में फिट होगी।
जेरज़ी लॉस लॉजिक को उनके 1947 के मास्टर की थीसिस द फ़ाउंडेशन ऑफ़ ए मेथोडोलॉजिकल एनालिसिस ऑफ़ मिल्स मेथड्स के रूप में प्रकाशित किया गया था।<ref name="Tkaczyk 2019 259–276">{{Cite journal|last1=Tkaczyk|first1=Marcin|last2=Jarmużek|first2=Tomasz|date=2019|title=Jerzy Łoś Positional Calculus and the Origin of Temporal Logic|url=https://apcz.umk.pl/LLP/article/view/LLP.2018.013|journal=Logic and Logical Philosophy|language=en|volume=28|issue=2|pages=259–276|doi=10.12775/LLP.2018.013|issn=2300-9802|doi-access=free}}</ref> उनकी दार्शनिक और औपचारिक अवधारणाओं को लविव-वारसॉ स्कूल ऑफ़ लॉजिक की निरंतरता के रूप में देखा जा सकता है, क्योंकि उनके पर्यवेक्षक जेरज़ी स्लूपेकी थे, जो जन लुकासिविक्ज़ के शिष्य थे। पेपर का 1977 तक अंग्रेजी में अनुवाद नहीं किया गया था, हालांकि हेनरिक हाईज़ ने 1951 में एक संक्षिप्त, लेकिन सूचनात्मक, [[प्रतीकात्मक तर्क का जर्नल|प्रतीकात्मक लॉजिक का जर्नल]] में समीक्षा प्रस्तुत की। इस समीक्षा में जेरज़ी लॉस के काम की मूल अवधारणाएँ सम्मिलित थीं और तार्किक समुदाय के बीच उनके परिणामों को लोकप्रिय बनाने के लिए पर्याप्त थीं। इस कार्य का मुख्य उद्देश्य मिल के सिद्धांतों को औपचारिक लॉजिक के ढांचे में प्रस्तुत करना था। इस लक्ष्य को प्राप्त करने के लिए लेखक ने मिल की अवधारणा की संरचना में लौकिक कार्यों के महत्व पर शोध किया। ऐसा करने के बाद, उन्होंने लॉजिक की अपनी स्वयंसिद्ध प्रणाली प्रदान की जो मिल के सिद्धांतों के साथ-साथ उनके लौकिक पहलुओं के लिए एक रूपरेखा के रूप में फिट होगी।


=== सिंटेक्स ===
=== सिंटेक्स ===
पोडस्टावी एनालिज़ी मेटोडोलॉजिक्ज़नेज कानोनोव मिल्ला (द फ़ाउंडेशन ऑफ़ ए मेथोडोलॉजिकल एनालिसिस ऑफ़ मिल्स मेथड्स) में पहली बार प्रकाशित तर्क की भाषा में सम्मिलित हैं:<ref name=":0" />
पोडस्टावी एनालिज़ी मेटोडोलॉजिक्ज़नेज कानोनोव मिल्ला (द फ़ाउंडेशन ऑफ़ ए मेथोडोलॉजिकल एनालिसिस ऑफ़ मिल्स मेथड्स) में पहली बार प्रकाशित लॉजिक की भाषा में सम्मिलित हैं:<ref name=":0" />


* पहले क्रम के लॉजिक ऑपरेटर्स  '¬', '∧', '∨', '→', '≡', '∀' और '∃'
* पहले क्रम के लॉजिक ऑपरेटर्स  '¬', '∧', '∨', '→', '≡', '∀' और '∃'
* प्राप्ति संचालक यू
* प्राप्ति संचालक U
* कार्यात्मक प्रतीक δ
* कार्यात्मक प्रतीक δ
* प्रस्तावक चर पी<sub>1</sub>,पी<sub>2</sub>,पी<sub>3</sub>,...
* प्रस्तावक चर p<sub>1</sub>,p<sub>2</sub>,p<sub>3</sub>,...
* समय के क्षणों को निरूपित करने वाले चर टी<sub>1</sub>,टी<sub>2</sub>,टी<sub>3</sub>,...
* समय के क्षणों को निरूपित करने वाले चर t<sub>1</sub>,t<sub>2</sub>,t<sub>3</sub>,...
* समय अंतराल n को निरूपित करने वाले चर<sub>1</sub>,एन<sub>2</sub>,एन<sub>3</sub>,...
* समय अंतराल को निरूपित करने वाले चर n<sub>1</sub>,n<sub>2</sub>,n<sub>3</sub>,...


शर्तों का सेट (एस द्वारा चिह्नित) निम्नानुसार बनाया गया है:
शर्तों का सेट (S द्वारा चिह्नित) निम्नानुसार बनाया गया है:


* समय के क्षणों या अंतराल को दर्शाने वाले चर शब्द हैं
* समय के क्षणों या अंतराल को दर्शाने वाले चर शब्द हैं
* अगर <math>\tau \in S</math> और <math>\epsilon</math> एक समय अंतराल चर है, तो <math>\delta(\tau, \epsilon) \in S</math>
* अगर <math>\tau \in S</math> और <math>\epsilon</math> एक समय अंतराल चर है, तो <math>\delta(\tau, \epsilon) \in S</math>
सूत्रों का सेट (जिसे फॉर द्वारा दर्शाया गया है) इस प्रकार बनाया गया है:<ref name= Tkaczyk 2019 259–276 />
सूत्रों का सेट (जिसे फॉर द्वारा दर्शाया गया है) इस प्रकार बनाया गया है:


* सभी प्रथम-क्रम तर्क सूत्र मान्य हैं
* सभी प्रथम-क्रम लॉजिक सूत्र मान्य हैं
* अगर <math>\tau \in S</math> और <math>\phi</math> एक प्रस्तावक चर है, फिर <math>U_{\tau}(\phi) \in For</math>
* अगर <math>\tau \in S</math> और <math>\phi</math> एक प्रस्तावक चर है, फिर <math>U_{\tau}(\phi) \in For</math>
* अगर <math>\phi \in For</math>, तब <math>\neg \phi \in For</math>
* अगर <math>\phi \in For</math>, तब <math>\neg \phi \in For</math>
* अगर <math>\phi, \psi \in For</math> और <math>\circ \in \{\wedge, \vee, \rightarrow, \equiv\}</math>, तब <math>\phi \circ \psi \in For</math>
* अगर <math>\phi, \psi \in For</math> और <math>\circ \in \{\wedge, \vee, \rightarrow, \equiv\}</math>, तब <math>\phi \circ \psi \in For</math>
* अगर <math>\phi \in For</math> और <math>Q \in \{\forall, \exists\}</math> और υ तब एक प्रस्तावात्मक, क्षण या अंतराल चर है <math>Q_{\upsilon}\phi \in For</math>
* अगर <math>\phi \in For</math> और <math>Q \in \{\forall, \exists\}</math> और υ तब एक प्रस्तावात्मक, क्षण या अंतराल चर है <math>Q_{\upsilon}\phi \in For</math>
=== मूल स्वयंसिद्ध प्रणाली ===
=== मूल स्वयंसिद्ध प्रणाली ===


Line 60: Line 72:
# <math>\forall_{t_{1}}\exists_{p_{1}}\forall_{t_{2}}(U_{t_{2}} p_{1}  
# <math>\forall_{t_{1}}\exists_{p_{1}}\forall_{t_{2}}(U_{t_{2}} p_{1}  
\equiv \forall_{p_{2}}(U_{t_{1}}p_{2} \equiv U_{t_{2}}p_{2}))</math>
\equiv \forall_{p_{2}}(U_{t_{1}}p_{2} \equiv U_{t_{2}}p_{2}))</math>
== पूर्व काल का तर्क (टीएल) ==
 
टाइम एंड मॉडेलिटी में पेश किए गए वाक्यात्मक काल तर्क में चार (गैर-सत्य कार्य | सत्य-कार्यात्मक) मोडल ऑपरेटर हैं (प्रस्तावात्मक कलन में सभी सामान्य सत्य-कार्यात्मक ऑपरेटरों के अलावा | प्रथम-क्रम प्रस्तावपरक तर्क)।<ref>{{Cite book|title=Time and modality: the John Locke lectures for 1955–6, delivered at the University of Oxford|last=Prior|first=Arthur Norman|publisher=The Clarendon Press|year=2003|isbn=9780198241584|location=Oxford|oclc=905630146|author-link=Arthur Prior}}</ref>
[[Category:CS1 English-language sources (en)]]
* पी: यह मामला था कि... (पी अतीत के लिए खड़ा है)
[[Category:Collapse templates]]
* एफ: यह मामला होगा कि ... (एफ भविष्य के लिए खड़ा है)
[[Category:Commons category link is the pagename]]
* जी: प्रायः ऐसा ही रहेगा कि...
[[Category:Created On 02/03/2023]]
* एच: प्रायः ऐसा होता था कि...
[[Category:Machine Translated Page]]
[[Category:Navigational boxes| ]]
[[Category:Navigational boxes without horizontal lists]]
[[Category:Pages with broken file links]]
[[Category:Pages with empty portal template]]
[[Category:Pages with reference errors]]
[[Category:Pages with script errors]]
[[Category:Portal templates with redlinked portals]]
[[Category:Templates Vigyan Ready]]
 
== पूर्व काल का लॉजिक (टीएल) ==
टाइम एंड मॉडेलिटी में पेश किए गए वाक्यात्मक काल लॉजिक में चार (गैर-सत्य कार्य | सत्य-कार्यात्मक) मोडल ऑपरेटर हैं (प्रस्तावात्मक कलन में सभी सामान्य सत्य-कार्यात्मक ऑपरेटरों के अलावा | प्रथम-क्रम प्रस्तावपरक लॉजिक)।<ref>{{Cite book|title=Time and modality: the John Locke lectures for 1955–6, delivered at the University of Oxford|last=Prior|first=Arthur Norman|publisher=The Clarendon Press|year=2003|isbn=9780198241584|location=Oxford|oclc=905630146|author-link=Arthur Prior}}</ref>
* ''P'': यह मामला था कि... (P अतीत के लिए खड़ा है)
* ''F'': यह मामला होगा कि ... (F भविष्य के लिए खड़ा है)
* ''G'': प्रायः ऐसा ही रहेगा कि...
* ''H'': प्रायः ऐसा होता था कि...


इन्हें संयुक्त किया जा सकता है यदि हम π को एक अनंत पथ होने दें:<ref>{{Cite web|url=https://www.cas.mcmaster.ca/~lawford/2F03/Notes/model.pdf|title=टेम्पोरल लॉजिक्स का एक परिचय|last=Lawford|first=M.|date=2004|website=Department of Computer Science McMaster University}}</ref>
इन्हें संयुक्त किया जा सकता है यदि हम π को एक अनंत पथ होने दें:<ref>{{Cite web|url=https://www.cas.mcmaster.ca/~lawford/2F03/Notes/model.pdf|title=टेम्पोरल लॉजिक्स का एक परिचय|last=Lawford|first=M.|date=2004|website=Department of Computer Science McMaster University}}</ref>
Line 83: Line 110:
<math>\phi,\psi ::= a \;|\; \bot \;|\; \lnot\phi \;|\; \phi\lor\psi \;|\; G\phi \;|\; H\phi</math>
<math>\phi,\psi ::= a \;|\; \bot \;|\; \lnot\phi \;|\; \phi\lor\psi \;|\; G\phi \;|\; H\phi</math>
जहाँ ए  कुछ [[परमाणु सूत्र]] है।<ref>{{Cite book|url=https://plato.stanford.edu/archives/win2015/entries/logic-temporal/|title=द स्टैनफोर्ड एनसाइक्लोपीडिया ऑफ फिलॉसफी|last1=Goranko|first1=Valentin|last2=Galton|first2=Antony|date=2015|publisher=Metaphysics Research Lab, Stanford University|editor-last=Zalta|editor-first=Edward N.|edition=Winter 2015}}</ref>
जहाँ ए  कुछ [[परमाणु सूत्र]] है।<ref>{{Cite book|url=https://plato.stanford.edu/archives/win2015/entries/logic-temporal/|title=द स्टैनफोर्ड एनसाइक्लोपीडिया ऑफ फिलॉसफी|last1=Goranko|first1=Valentin|last2=Galton|first2=Antony|date=2015|publisher=Metaphysics Research Lab, Stanford University|editor-last=Zalta|editor-first=Edward N.|edition=Winter 2015}}</ref>
टीएल में [[वाक्य (गणितीय तर्क)]] की सच्चाई का मूल्यांकन करने के लिए [[कृपके शब्दार्थ]] का उपयोग किया जाता है। एक जोड़ी ({{Var|T}}, <) एक सेट के {{Var|T}} और एक [[द्विआधारी संबंध]] <पर {{Var|T}} (प्राथमिकता कहा जाता है) को एक फ्रेम कहा जाता है। एक मॉडल ट्रिपल द्वारा दिया गया है ({{Var|T}}, <, {{Var|V}}) एक फ्रेम और एक फ़ंक्शन का {{Var|V}} एक मूल्यांकन कहा जाता है जो प्रत्येक जोड़ी को निर्दिष्ट करता है ({{Var|a}}, {{Var|u}}) एक परमाणु सूत्र और एक समय मूल्य कुछ सत्य मान। धारणा{{Var|ϕ}} एक मॉडल में सच है {{Var|U}}=({{Var|T}}, <, {{Var|V}}) समय पर {{Var|u}} संक्षिप्त है {{var|U}}डबल घूमने वाला दरवाज़ा|⊨{{var|ϕ}}[{{var|u}}]। इस अंकन के साथ,<ref>{{Cite book|title=दार्शनिक तर्क का सातत्य साथी|last=Müller|first=Thomas|publisher=A&C Black|year=2011|editor-last=Horsten|editor-first=Leon|pages=329|chapter=Tense or temporal logic|chapter-url=http://kops.uni-konstanz.de/bitstream/handle/123456789/27232/Mueller_272322.pdf?sequence=2}}</ref>
टीएल में [[वाक्य (गणितीय तर्क)|वाक्य (गणितीय लॉजिक)]] की सच्चाई का मूल्यांकन करने के लिए [[कृपके शब्दार्थ]] का उपयोग किया जाता है। एक जोड़ी ({{Var|T}}, <) एक सेट के {{Var|T}} और एक [[द्विआधारी संबंध]] <पर {{Var|T}} (प्राथमिकता कहा जाता है) को एक फ्रेम कहा जाता है। एक मॉडल ट्रिपल द्वारा दिया गया है ({{Var|T}}, <, {{Var|V}}) एक फ्रेम और एक फ़ंक्शन का {{Var|V}} एक मूल्यांकन कहा जाता है जो प्रत्येक जोड़ी को निर्दिष्ट करता है ({{Var|a}}, {{Var|u}}) एक परमाणु सूत्र और एक समय मूल्य कुछ सत्य मान। धारणा{{Var|ϕ}} एक मॉडल में सच है {{Var|U}}=({{Var|T}}, <, {{Var|V}}) समय पर {{Var|u}} संक्षिप्त है {{var|U}}डबल घूमने वाला दरवाज़ा|⊨{{var|ϕ}}[{{var|u}}]। इस अंकन के साथ,<ref>{{Cite book|title=दार्शनिक तर्क का सातत्य साथी|last=Müller|first=Thomas|publisher=A&C Black|year=2011|editor-last=Horsten|editor-first=Leon|pages=329|chapter=Tense or temporal logic|chapter-url=http://kops.uni-konstanz.de/bitstream/handle/123456789/27232/Mueller_272322.pdf?sequence=2}}</ref>


{| class="wikitable"
{| class="wikitable"
Line 106: Line 133:
|-
|-
| {{var|U}}⊨G{{var|ϕ}}[{{var|u}}]
| {{var|U}}⊨G{{var|ϕ}}[{{var|u}}]
| {{var|U}}⊨{{var|ϕ}}[{{var|v}}] for ए ll {{var|v}} with {{var|u}}<{{var|v}}
| {{var|U}}⊨{{var|ϕ}}[{{var|v}}] for all {{var|v}} with {{var|u}}<{{var|v}}
|-
|-
| {{var|U}}⊨H{{var|ϕ}}[{{var|u}}]
| {{var|U}}⊨H{{var|ϕ}}[{{var|u}}]
| {{var|U}}⊨{{var|ϕ}}[{{var|v}}] for ए ll {{var|v}} with {{var|v}}<{{var|u}}
| {{var|U}}⊨{{var|ϕ}}[{{var|v}}] for all {{var|v}} with {{var|v}}<{{var|u}}
|}
|}
फ़्रेम के वर्ग F को देखते हुए, TL का एक वाक्य ϕ है
फ़्रेम के वर्ग ''F'' को देखते हुए, TL का एक वाक्य ϕ है


* एफ के संबंध में वैध अगर प्रत्येक मॉडल यू = (टी, <, वी) के साथ (टी, <) एफ में और प्रत्येक यू के लिए टी में, यू⊨ϕ [यू]
* ''F'' के संबंध में वैध अगर प्रत्येक मॉडल U = (T, <, V) के साथ (T, <) ''F'' में और प्रत्येक u के लिए T में, U⊨ϕ [u]
* एफ के संबंध में संतोषजनक अगर एक मॉडल यू = (टी, <, वी) के साथ (टी, <) एफ में ऐसा है कि टी में कुछ यू के लिए, यू⊨ϕ [यू]
* ''F'' के संबंध में संतोषजनक अगर एक मॉडल U = (''T'', <, V) के साथ (T, <) ''F'' में ऐसा है कि T में कुछ u के लिए, U⊨ϕ [u]
* एफ के संबंध में एक वाक्य ψ का परिणाम यदि प्रत्येक मॉडल के लिए U=(T,<,V) के साथ (T,<) F में और प्रत्येक u के लिए T में, यदि U⊨ψ[u], तो U⊨ϕ [यू]
* ''F'' के संबंध में एक वाक्य ψ का परिणाम यदि प्रत्येक मॉडल के लिए U=(T,<,V) के साथ (T,<) F में और प्रत्येक u के लिए T में, यदि U⊨ψ[u], तो U⊨ϕ [u]


कई वाक्य केवल सीमित वर्ग के फ्रेम के लिए मान्य हैं। फ्रेम के वर्ग को उन लोगों तक सीमित करना आम है जिनके संबंध हैं < जो [[सकर्मक कमी]], [[ एंटीसिमेट्रिक संबंध ]], [[अल्हड़]] रिलेशन, [[ट्राइकोटॉमी (गणित)]], अपरिवर्तनीय, [[कुल आदेश]], घने क्रम, या इनमें से कुछ संयोजन है।
कई वाक्य केवल सीमित वर्ग के फ्रेम के लिए मान्य हैं। फ्रेम के वर्ग को उन लोगों तक सीमित करना आम है जिनके संबंध हैं < जो [[सकर्मक कमी]], [[ एंटीसिमेट्रिक संबंध ]], [[अल्हड़]] रिलेशन, [[ट्राइकोटॉमी (गणित)]], अपरिवर्तनीय, [[कुल आदेश]], घने क्रम, या इनमें से कुछ संयोजन है।


=== एक न्यूनतम स्वयंसिद्ध तर्क ===
=== एक न्यूनतम स्वयंसिद्ध लॉजिक ===
बर्गेस एक ऐसे तर्क को रेखांकित करता है जो संबंध <पर कोई धारणा नहीं बनाता है, लेकिन निम्नलिखित स्वयंसिद्ध स्कीमा के आधार पर सार्थक कटौती की अनुमति देता है: [15]
बर्गेस एक ऐसे लॉजिक को रेखांकित करता है जो संबंध < पर कोई धारणा नहीं बनाता है, लेकिन निम्नलिखित स्वयंसिद्ध स्कीमा के आधार पर सार्थक कटौती की अनुमति देता है: [15]


# ए जहां ए प्रथम-क्रम तर्क का पुनरुत्पादन [[टॉटोलॉजी (तर्क)]] है
# ''A'' जहां ''A'' प्रथम-क्रम लॉजिक का पुनरुत्पादन [[टॉटोलॉजी (तर्क)|टॉटोलॉजी (लॉजिक)]]  
# जी (ए → बी) → (जीए → जीबी)
#(<var>A</var>→<var>B</var>)→(G<var>A</var>→G<var>B</var>)
# एच (ए → बी) → (एचए → एचबी)
#H(<var>A</var>→<var>B</var>)→(H<var>A</var>→H<var>B</var>)
# ए → जीपीए ए → एचएफए
#<var>A</var>→GP<var>A</var>
#<var>A</var>→HF<var>A</var>


कटौती के निम्नलिखित नियमों के साथ:
कटौती के निम्नलिखित नियमों के साथ:


# दिए गए ए → बी और ए , घटाएँ बी (एक वैध, सरल तर्क और निष्कर्ष के नियम के रूप)
# दिए गए <var>A</var>→<var>B</var> और <var>A</var>, घटाएँ ''B'' (एक वैध, सरल लॉजिक और निष्कर्ष के नियम के रूप)
# एक टॉटोलॉजी ए दी गई, जीए का अनुमान लगाएं
# एक टॉटोलॉजी ''A'' दी गई, G<var>A</var> का अनुमान लगाएं
# एक टॉटोलॉजी ए दिया, अनुमान हा
# एक टॉटोलॉजी ''A'' दिया, अनुमान हा


कोई निम्नलिखित नियम प्राप्त कर सकता है
कोई निम्नलिखित नियम प्राप्त कर सकता है
# बेकर का नियम: दिया गया {{var|ए}}→{{var|बी}}, टीनिकालिए ए → टी बी जहां टी एक काल है, जी, एच, एफ, और पी से बना कोई भी अनुक्रमणिका।
# '''बेकर का नियम''': दिया गया <var>A</var>→<var>B</var>, घटाएँ TA → TB जहां T एक काल है, G, H, F, और P से बना कोई भी अनुक्रमणिका।
# मिररिंग: एक प्रमेय दिया गया ए, इसका दर्पण कथन निकालिए ए§, जो जी को एच से (और इसलिए एफ को पी से) और इसके विपरीत करके प्राप्त किया जाता है।
# '''मिररिंग''': एक प्रमेय दिया गया ''A'', इसका दर्पण कथन निकालिए <var>A</var><sup>§</sup>, जो ''G'' को H से (और इसलिए F को P से) और इसके विपरीत करके प्राप्त किया जाता है।
# द्वैत: एक प्रमेय दिया गया ए, इसकी दोहरा कथन कथन ए*, जो ∧ को ∨ से, जी को एफ से, और एच को पी से धारणा प्राप्त की जाती है।
# '''द्वैत''': एक प्रमेय दिया गया ''A'', इसकी '''दोहरा कथन''' कथन ''A''*, जो ∧ को ∨ से, ''G'' को F से, और H को P से धारणा प्राप्त की जाती है।


=== विधेय तर्क के लिए अनुवाद ===
=== विधेय लॉजिक के लिए अनुवाद ===
बर्गेस टीएल में बयानों से एक मुक्त चर के साथ प्रथम-क्रम तर्क में बयानों में मेरेडिथ अनुवाद देता है {{Var|x}}<sub>0</sub> (वर्तमान क्षण का प्रतिनिधित्व)। यह अनुवाद {{Var|M}} को पुनरावर्ती रूप से निम्नानुसार परिभाषित किया गया है:<ref>{{Cite book|title=दार्शनिक तर्क|last=Burgess|first=John P.|publisher=Princeton University Press|year=2009|isbn=9781400830497|location=Princeton, New Jersey|page=17|oclc=777375659|author-link=John P. Burgess}}</ref>
बर्गेस टीएल में बयानों से एक मुक्त चर के साथ प्रथम-क्रम लॉजिक में बयानों में मेरेडिथ अनुवाद देता है {{Var|x}}<sub>0</sub> (वर्तमान क्षण का प्रतिनिधित्व)। यह अनुवाद {{Var|M}} को पुनरावर्ती रूप से निम्नानुसार परिभाषित किया गया है:<ref>{{Cite book|title=दार्शनिक तर्क|last=Burgess|first=John P.|publisher=Princeton University Press|year=2009|isbn=9781400830497|location=Princeton, New Jersey|page=17|oclc=777375659|author-link=John P. Burgess}}</ref>


<math>\begin{align}
<math>\begin{align}
Line 156: Line 184:
{| class="wikitable"
{| class="wikitable"
|-
|-
! Textuए l
! शाब्दिक
! Symबीolic
! प्रतीकात्मक
! Definition
! परिभाषा
! Explए nए tion
! व्याख्या
! Diए grए m
! आरेख
|-
|-
! colspan="4" | [[Binary operator|बीinए ry operए tor]]s
! colspan="4" | बाइनरी ऑपरेटर्स
|-
|-
|{{mvar|&phi;}} '''U''' {{mvar|&psi;}}
|{{mvar|&phi;}} '''U''' {{mvar|&psi;}}
|<math>\phi ~\mathcal{U}~ \psi</math>
|<math>\phi ~\mathcal{U}~ \psi</math>
|<math>(B\,\mathcal{U}\,C)(\phi)= \ (\exists i:C(\phi_i)\land(\forall j<i:B(\phi_j)))</math>
|<math>(B\,\mathcal{U}\,C)(\phi)= \ (\exists i:C(\phi_i)\land(\forall j<i:B(\phi_j)))</math>
|'''U'''ntil: {{mvar|&psi;}} holds ए t the current or ए  future position, ए nd {{mvar|&phi;}} hए s to hold until thए t position. ए t thए t position {{mvar|&phi;}} does not hए ve to hold ए ny more.
|'''तब''' तक (Untill): ψ वर्तमान या भविष्य की स्थिति पर कायम रहता है, और φ को उस स्थिति तक बने रहना होता है। उस स्थिति में φ को और अधिक धारण करने की आवश्यकता नहीं है।
|<timeline>
|[[File:Timeline6.png|center]]
Imए geSize = width:240 height:94
Plotए reए  = left:30 बीottom:30 top:0 right:20
Dए teFormए t = x.y
Period = from:0 till:6
Timeए xis = orientए tion:horizontए l
ए lignबीए rs = justify
Scए leMए jor = gridcolor:बीlए ck increment:1 stए rt:0
Scए leMinor = gridcolor:बीlए ck increment:1 stए rt:0
 
PlotDए tए =
बीए r:p color:red width:10 ए lign:left fontsize:S
from:1 till:3
 
बीए r:q color:red width:10 ए lign:left fontsize:S
from:3 till:5
 
बीए r:pUq color:red width:10 ए lign:left fontsize:S
from:1 till:5
</timeline>
|-
|-
|{{mvar|&phi;}} '''R''' {{mvar|&psi;}}
|{{mvar|&phi;}} '''R''' {{mvar|&psi;}}
|<math>\phi ~\mathcal{R}~ \psi</math>
|<math>\phi ~\mathcal{R}~ \psi</math>
|<math>(B\,\mathcal{R}\,C)(\phi)= \ (\forall i:C(\phi_i)\lor(\exists j<i:B(\phi_j)))</math>
|<math>(B\,\mathcal{R}\,C)(\phi)= \ (\forall i:C(\phi_i)\lor(\exists j<i:B(\phi_j)))</math>
|'''R'''eleए se: {{mvar|&phi;}} releए ses {{mvar|&psi;}} if {{mvar|&psi;}} is true up until ए nd including the first position in which {{mvar|&phi;}} is true (or forever if such ए  position does not exist).
|'''R''' elease: φ ψ जारी करता है यदि ψ सत्य है और इसमें पहली स्थिति सम्मिलित है जिसमें φ सत्य है (या हमेशा के लिए यदि ऐसी स्थिति सम्मिलित नहीं है)।
|<timeline>
|[[File:Timeline2.png|center]]
Imए geSize = width:240 height:100
Plotए reए  = left:30 बीottom:30 top:0 right:20
Dए teFormए t = x.y
Period = from:0 till:8
Timeए xis = orientए tion:horizontए l
ए lignबीए rs = justify
Scए leMए jor = gridcolor:बीlए ck increment:1 stए rt:0
Scए leMinor = gridcolor:बीlए ck increment:1 stए rt:0
 
PlotDए tए =
बीए r:p color:red width:10 ए lign:left fontsize:S
from:2 till:4
from:6 till:8
 
बीए r:q color:red width:10 ए lign:left fontsize:S
from:1 till:3
from:5 till:6
from:7 till:8
 
बीए r:pRq color:red width:10 ए lign:left fontsize:S
from:1 till:3
from:7 till:8
</timeline>
|-
|-
! colspan="4" | [[Unary operator|Unए ry operए tor]]s
! colspan="4" | [[Unary operator|यूनरी ऑपरेटर्स]]
|-
|-
|'''N''' {{mvar|&phi;}}
|'''N''' {{mvar|&phi;}}
|<math>\bigcirc \phi</math>
|<math>\bigcirc \phi</math>
|<math>\mathcal{N}B(\phi_i)=B(\phi_{i+1})</math>
|<math>\mathcal{N}B(\phi_i)=B(\phi_{i+1})</math>
|'''N'''ext: {{mvar|&phi;}} hए s to hold ए t the next stए te. ('''X''' is used synonymously.)
|'''N''' ext: φ को अगले राज्य में रखना है। ( '''एक्स''' समानार्थक रूप से प्रयोग किया जाता है।)
|<timeline>
|[[File:Timeline3.png|center]]
Imए geSize = width:240 height:60
Plotए reए  = left:30 बीottom:30 top:0 right:20
Dए teFormए t = x.y
Period = from:0 till:6
Timeए xis = orientए tion:horizontए l
ए lignबीए rs = justify
Scए leMए jor = gridcolor:बीlए ck increment:1 stए rt:0
Scए leMinor = gridcolor:बीlए ck increment:1 stए rt:0
 
PlotDए tए =
बीए r:p color:red width:10 ए lign:left fontsize:S
from:2 till:3
from:5 till:6
 
बीए r:Np color:red width:10 ए lign:left fontsize:S
from:1 till:2
from:4 till:5
</timeline>
|-
|-
|'''F''' {{mvar|&phi;}}
|'''F''' {{mvar|&phi;}}
|<math>\Diamond \phi</math>
|<math>\Diamond \phi</math>
|<math>\mathcal{F}B(\phi)=(true\,\mathcal{U}\,B)(\phi)</math>
|<math>\mathcal{F}B(\phi)=(true\,\mathcal{U}\,B)(\phi)</math>
|'''F'''uture: {{mvar|&phi;}} eventuए lly hए s to hold (somewhere on the suबीsequent pए th).
|'''Future''' : φ को अंततः पकड़ना होगा (कहीं बाद के रास्ते पर)।
|<timeline>
|[[File:Timeline4.png|center]]
Imए geSize = width:240 height:60
Plotए reए  = left:30 बीottom:30 top:0 right:20
Dए teFormए t = x.y
Period = from:0 till:6
Timeए xis = orientए tion:horizontए l
ए lignबीए rs = justify
Scए leMए jor = gridcolor:बीlए ck increment:1 stए rt:0
Scए leMinor = gridcolor:बीlए ck increment:1 stए rt:0
 
PlotDए tए =
बीए r:p color:red width:10 ए lign:left fontsize:S
from:2 till:3
from:4 till:5
 
बीए r:Fp color:red width:10 ए lign:left fontsize:S
from:0 till:5
</timeline>
|-
|-
|'''G''' {{mvar|&phi;}}
|'''G''' {{mvar|&phi;}}
|<math>\Box \phi</math>
|<math>\Box \phi</math>
|<math>\mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi)</math>
|<math>\mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi)</math>
|'''G'''loबीए lly: {{mvar|&phi;}} hए s to hold on the entire suबीsequent pए th.
|'''G'''lobally: φ को बाद के पूरे रास्ते पर पकड़ बनानी है।
|<timeline>
|[[File:Timeline5-latest.png|center|thumb]]
Imए geSize = width:240 height:60
Plotए reए  = left:30 बीottom:30 top:0 right:20
Dए teFormए t = x.y
Period = from:0 till:6
Timeए xis = orientए tion:horizontए l
ए lignबीए rs = justify
Scए leMए jor = gridcolor:बीlए ck increment:1 stए rt:0
Scए leMinor = gridcolor:बीlए ck increment:1 stए rt:0
 
PlotDए tए =
बीए r:p color:red width:10 ए lign:left fontsize:S
from:1 till:3
from:4 till:6
 
बीए r:Gp color:red width:10 ए lign:left fontsize:S
from:4 till:6
</timeline>
|-
|-
|'''ए'''  {{mvar|&phi;}}
|'''A'''  {{mvar|&phi;}}
|<math>\forall \phi</math>
|<math>\forall \phi</math>
|<math>(\mathcal{A}B)(\psi)= \ (\forall \phi:\phi_0=\psi\to B(\phi))</math>
|<math>(\mathcal{A}B)(\psi)= \ (\forall \phi:\phi_0=\psi\to B(\phi))</math>
|'''ए''' ll: {{mvar|&phi;}} hए s to hold on ए ll pए ths stए rting from the current stए te.
|'''A'''ll: φ को वर्तमान स्थिति से प्रांरम्भ होने वाले सभी पथों पर पकड़ बनाना है।
|
|
|-
|-
Line 299: Line 233:
|<math>\exists \phi</math>
|<math>\exists \phi</math>
|<math>(\mathcal{E}B)(\psi)= \ (\exists \phi:\phi_0=\psi\land B(\phi))</math>
|<math>(\mathcal{E}B)(\psi)= \ (\exists \phi:\phi_0=\psi\land B(\phi))</math>
|'''E'''xists: there exists ए t leए st one pए th stए rting from the current stए te where {{mvar|&phi;}} holds.
|'''E'''xists: वर्तमान स्थिति से प्रारम्भ होने वाला कम से कम एक पथ सम्मिलित है जहां φ धारण करता है।
|
|
|}
|}
वैकल्पिक प्रतीक:
वैकल्पिक प्रतीक:


* ऑपरेटर आर को कभी-कभी वी द्वारा निरूपित किया जाता है
* ऑपरेटर '''R''' को कभी-कभी '''V''' द्वारा निरूपित किया जाता है
* ऑपरेटर डब्ल्यू'' तक कमजोर '' ऑपरेटर है: <math>f \mathbf W g</math> के बराबर है <math>f \mathbf U g \lor \mathbf G f</math>
* ऑपरेटर '''W''''' तक कमजोर ''ऑपरेटर है: <math>f \mathbf W g</math> के बराबर है <math>f \mathbf U g \lor \mathbf G f</math>
यूनरी ऑपरेटर जब भी अच्छी तरह से बने सूत्र होते हैं {{math|B({{var|&phi;}})}} सुगठित है। जब भी बाइनरी ऑपरेटर अच्छी तरह से गठित सूत्र होते हैं {{math|B({{var|&phi;}})}} और {{math|C({{var|&phi;}})}} सुगठित हैं।
यूनरी ऑपरेटर जब भी अच्छी तरह से बने सूत्र होते हैं {{math|B({{var|&phi;}})}} सुगठित है। जब भी बाइनरी ऑपरेटर अच्छी तरह से गठित सूत्र होते हैं {{math|B({{var|&phi;}})}} और {{math|C({{var|&phi;}})}} सुगठित हैं।


कुछ लॉजिक्स में, कुछ ऑपरेटरों को व्यक्त नहीं किया जा सकता है। उदाहरण के लिए, एन ऑपरेटर को क्रियाओं के अस्थायी तर्क में व्यक्त नहीं किया जा सकता है।
कुछ लॉजिक्स में, कुछ ऑपरेटरों को व्यक्त नहीं किया जा सकता है। उदाहरण के लिए, एन ऑपरेटर को क्रियाओं के अस्थायी लॉजिक में व्यक्त नहीं किया जा सकता है।
 
== टेम्पोरल लॉजिक्स ==
== टेम्पोरल लॉजिक्स ==
टेम्पोरल लॉजिक्स में सम्मिलित हैं:
टेम्पोरल लॉजिक्स में सम्मिलित हैं:


* [[स्थितीय तर्क]] की कुछ प्रणालियाँ
* [[स्थितीय तर्क|स्थितीय लॉजिक]] की कुछ प्रणालियाँ
* लीनियर टेम्पोरल लॉजिक (एलटीएल [[अंतराल लौकिक तर्क]] बिना ब्रांचिंग टाइमलाइन के
* लीनियर टेम्पोरल लॉजिक (एलटीएल [[अंतराल लौकिक तर्क|अंतराल टेम्पोरल लॉजिक]] बिना ब्रांचिंग टाइमलाइन के
* कम्प्यूटेशन ट्री लॉजिक (सीटीएल) टेम्पोरल लॉजिक ब्रांचिंग टाइमलाइन के साथ
* कम्प्यूटेशन ट्री लॉजिक (सीटीएल) टेम्पोरल लॉजिक ब्रांचिंग टाइमलाइन के साथ
* अंतराल अस्थायी तर्क (आईटीएल)
* अंतराल अस्थायी लॉजिक (आईटीएल)
* कार्यों का अस्थायी तर्क (टीएलए)
* कार्यों का अस्थायी लॉजिक (टीएलए)
* [[सिग्नल टेम्पोरल लॉजिक]] (एसटीएल)<ref name="autogenerated2004"/>* [[टाइमस्टैम्प अस्थायी तर्क]] (टीटीएल)<ref>{{Cite journal|url=https://asu.pure.elsevier.com/en/publications/timestamp-temporal-logic-ttl-for-testing-the-timing-of-cyber-phys|doi=10.1145/3126510|title=साइबर-भौतिक प्रणालियों के समय के परीक्षण के लिए टाइमस्टैम्प टेम्पोरल लॉजिक (टीटीएल)।|year=2017|last1=Mehrabian|first1=Mohammadreza|last2=Khayatian|first2=Mohammad|last3=Shrivastava|first3=Aviral|last4=Eidson|first4=John C.|last5=Derler|first5=Patricia|last6=Andrade|first6=Hugo A.|last7=Li-Baboud|first7=Ya-Shian|last8=Griffor|first8=Edward|last9=Weiss|first9=Marc|last10=Stanton|first10=Kevin|journal=ACM Transactions on Embedded Computing Systems|volume=16|issue=5s|pages=1–20|s2cid=3570088|doi-access=free}}</ref>
* [[सिग्नल टेम्पोरल लॉजिक]] (एसटीएल)<ref name="autogenerated2004"/>* [[टाइमस्टैम्प अस्थायी तर्क|टाइमस्टैम्प अस्थायी लॉजिक]] (टीटीएल)<ref>{{Cite journal|url=https://asu.pure.elsevier.com/en/publications/timestamp-temporal-logic-ttl-for-testing-the-timing-of-cyber-phys|doi=10.1145/3126510|title=साइबर-भौतिक प्रणालियों के समय के परीक्षण के लिए टाइमस्टैम्प टेम्पोरल लॉजिक (टीटीएल)।|year=2017|last1=Mehrabian|first1=Mohammadreza|last2=Khayatian|first2=Mohammad|last3=Shrivastava|first3=Aviral|last4=Eidson|first4=John C.|last5=Derler|first5=Patricia|last6=Andrade|first6=Hugo A.|last7=Li-Baboud|first7=Ya-Shian|last8=Griffor|first8=Edward|last9=Weiss|first9=Marc|last10=Stanton|first10=Kevin|journal=ACM Transactions on Embedded Computing Systems|volume=16|issue=5s|pages=1–20|s2cid=3570088|doi-access=free}}</ref>
* [[संपत्ति विशिष्टता भाषा]] (पीएसएल)
* [[संपत्ति विशिष्टता भाषा]] (पीएसएल)
* [[सीटीएल*]], जो एलटीएल और सीटीएल का सामान्यीकरण करता है
* [[सीटीएल*]], जो एलटीएल और सीटीएल का सामान्यीकरण करता है
* हेनेसी-मिलनर लॉजिक (एचएमएल)
* हेनेसी-मिलनर लॉजिक (एचएमएल)
* मोडल μ-कैलकुलस, जिसमें एक सबसेट एचएमएल और सीटीएल के रूप में सम्मिलित है*
* मोडल μ-कैलकुलस, जिसमें एक सबसेट एचएमएल और सीटीएल के रूप में सम्मिलित है*
* [[मीट्रिक लौकिक तर्क]] (एमटीएल)<ref>Koymans, R. (1990). "Specifying real-time properties with metric temporal logic", ''Real-Time Systems'' '''2'''(4): 255–299. {{doi|10.1007/BF01995674}}.</ref>
* [[मीट्रिक लौकिक तर्क|मीट्रिक टेम्पोरल लॉजिक]] (एमटीएल)<ref>Koymans, R. (1990). "Specifying real-time properties with metric temporal logic", ''Real-Time Systems'' '''2'''(4): 255–299. {{doi|10.1007/BF01995674}}.</ref>
* [[मीट्रिक अंतराल लौकिक तर्क]] (एमआईटीएल)<ref name="autogenerated2004">Maler, O.; Nickovic, D. (2004). "Monitoring temporal properties of continuous signals". {{doi|10.1007/978-3-540-30206-3_12}}.</ref>
* [[मीट्रिक अंतराल लौकिक तर्क|मीट्रिक अंतराल टेम्पोरल लॉजिक]] (एमआईटीएल)<ref name="autogenerated2004">Maler, O.; Nickovic, D. (2004). "Monitoring temporal properties of continuous signals". {{doi|10.1007/978-3-540-30206-3_12}}.</ref>
* समयबद्ध प्रस्तावपरक लौकिक तर्क (टीपीटीएल)
* समयबद्ध प्रस्तावपरक टेम्पोरल लॉजिक (टीपीटीएल)
* [[ट्रंकेटेड लीनियर टेम्पोरल लॉजिक]] (टीएलटीएल)<ref>Li, Xiao, Cristian-Ioan Vasile, and Calin Belta. "Reinforcement learning with temporal logic rewards." {{doi|10.1109/IROS.2017.8206234}}</ref>
* [[ट्रंकेटेड लीनियर टेम्पोरल लॉजिक]] (टीएलटीएल)<ref>Li, Xiao, Cristian-Ioan Vasile, and Calin Belta. "Reinforcement learning with temporal logic rewards." {{doi|10.1109/IROS.2017.8206234}}</ref>
* [[हाइपर टेम्पोरल लॉजिक]] (हाइपरएलटीएल) <ref>{{Cite book|chapter-url=https://link.springer.com/chapter/10.1007/978-3-642-54792-8_15|doi = 10.1007/978-3-642-54792-8_15|chapter = Temporal Logics for Hyperproperties|title = सुरक्षा और विश्वास के सिद्धांत|series = Lecture Notes in Computer Science|year = 2014|last1 = Clarkson|first1 = Michael R.|last2 = Finkbeiner|first2 = Bernd|last3 = Koleini|first3 = Masoud|last4 = Micinski|first4 = Kristopher K.|last5 = Rabe|first5 = Markus N.|last6 = Sánchez|first6 = César|volume = 8414|pages = 265–284|isbn = 978-3-642-54791-1|s2cid = 8938993}}</ref>
* [[हाइपर टेम्पोरल लॉजिक]] (हाइपरएलटीएल) <ref>{{Cite book|chapter-url=https://link.springer.com/chapter/10.1007/978-3-642-54792-8_15|doi = 10.1007/978-3-642-54792-8_15|chapter = Temporal Logics for Hyperproperties|title = सुरक्षा और विश्वास के सिद्धांत|series = Lecture Notes in Computer Science|year = 2014|last1 = Clarkson|first1 = Michael R.|last2 = Finkbeiner|first2 = Bernd|last3 = Koleini|first3 = Masoud|last4 = Micinski|first4 = Kristopher K.|last5 = Rabe|first5 = Markus N.|last6 = Sánchez|first6 = César|volume = 8414|pages = 265–284|isbn = 978-3-642-54791-1|s2cid = 8938993}}</ref>
लौकिक या कालानुक्रमिक या काल तर्क से निकटता से संबंधित भिन्नता, टोपोलॉजी, स्थान या स्थानिक स्थिति पर आधारित मोडल लॉजिक्स हैं।<ref>{{Cite book | doi=10.1007/978-94-017-3546-9_13| chapter=Topological Logic| title=दार्शनिक तर्क में विषय| pages=229–249| year=1968| last1=Rescher| first1=Nicholas| isbn=978-90-481-8331-9}}</ref><ref>{{Cite book |doi = 10.1007/978-94-009-9407-2_9|chapter = A Modal Logic of Place|title = निकोलस रेस्चर का दर्शन|pages = 65–73|year = 1979|last1 = von Wright|first1 = Georg Henrik|isbn = 978-94-009-9409-6}}</ref>
लौकिक या कालानुक्रमिक या काल लॉजिक से निकटता से संबंधित भिन्नता, टोपोलॉजी, स्थान या स्थानिक स्थिति पर आधारित मोडल लॉजिक्स हैं।<ref>{{Cite book | doi=10.1007/978-94-017-3546-9_13| chapter=Topological Logic| title=दार्शनिक तर्क में विषय| pages=229–249| year=1968| last1=Rescher| first1=Nicholas| isbn=978-90-481-8331-9}}</ref><ref>{{Cite book |doi = 10.1007/978-94-009-9407-2_9|chapter = A Modal Logic of Place|title = निकोलस रेस्चर का दर्शन|pages = 65–73|year = 1979|last1 = von Wright|first1 = Georg Henrik|isbn = 978-94-009-9409-6}}</ref>
 
 
== यह भी देखें ==
== यह भी देखें ==
{{Portal|Philosophy}}
{{Portal|Philosophy}}
Line 339: Line 270:
* [[राज्य संक्रमण प्रणाली]]
* [[राज्य संक्रमण प्रणाली]]
* अवधि कलन (डीसी)
* अवधि कलन (डीसी)
* [[ हाइब्रिड तर्क ]]
* [[ हाइब्रिड तर्क | हाइब्रिड लॉजिक]]
* [[परिमित-राज्य सत्यापन में अस्थायी तर्क]]
* [[परिमित-राज्य सत्यापन में अस्थायी तर्क|परिमित-राज्य सत्यापन में अस्थायी लॉजिक]]
* [[Reo समन्वय भाषा]]
* [[Reo समन्वय भाषा]]
* मोडल लॉजिक
* मोडल लॉजिक
Line 347: Line 278:
==टिप्पणियाँ==
==टिप्पणियाँ==
{{reflist}}
{{reflist}}
==संदर्भ==
==संदर्भ==
* Mordechए i बीen-ए ri, Zohए r Mए nnए , ए mir Pnueli: ''[https://link.springer.com/article/10.1007/BF01257083 The Temporए l Logic of बीrए nching Time]''. POPL 1981: 164–176
* Mordechai Ben-Ari, Zohar Manna, Amir Pnueli: ''[https://link.springer.com/article/10.1007/BF01257083 The Temporal Logic of Branching Time]''. POPL 1981: 164–176
* ए mir Pnueli: ''[https://www.dimap.ufrn.br/~richard/pubs/dim0436/papers/pnueli_temporal_1977.pdf The Temporए l Logic of Progrए ms]'' FOCS 1977: 46–57
* Amir Pnueli: ''[https://www.dimap.ufrn.br/~richard/pubs/dim0436/papers/pnueli_temporal_1977.pdf The Temporal Logic of Programs]'' FOCS 1977: 46–57
* Venemए , Yde, 2001, "Temporए l Logic," in Goबीle, Lou, ed., ''The बीlए ckwell Guide to Philosophicए l Logic''. बीlए ckwell.
* Venema, Yde, 2001, "Temporal Logic," in Goble, Lou, ed., ''The Blackwell Guide to Philosophical Logic''. Blackwell.
* E. ए . Emerson ए nd Chin-Lए ung Lei, "[https://www.sciencedirect.com/science/article/pii/0167642387900360/pdf?md5=43227d5832bc2b176eb3de0da978418d&isDTMRedir=Y&pid=1-s2.0-0167642387900360-main.pdf&_valck=1 Modए lities for model checking: बीrए nching time logic strikes बीए ck]", in ''Science of Computer Progrए mming'' 8, pp.&nbsp;275–306, 1987.
* E. A. Emerson and Chin-Laung Lei, "[https://www.sciencedirect.com/science/article/pii/0167642387900360/pdf?md5=43227d5832bc2b176eb3de0da978418d&isDTMRedir=Y&pid=1-s2.0-0167642387900360-main.pdf&_valck=1 Modalities for model checking: branching time logic strikes back]", in ''Science of Computer Programming'' 8, pp.&nbsp;275–306, 1987.
* E. ए . Emerson, "[https://profs.info.uaic.ro/~masalagiu/pub/handbook3.pdf Temporए l ए nd modए l logic]", ''Hए ndबीook of Theoreticए l Computer Science'', Chए pter 16, the MIT Press, 1990
* E. A. Emerson, "[https://profs.info.uaic.ro/~masalagiu/pub/handbook3.pdf Temporal and modal logic]", ''Handbook of Theoretical Computer Science'', Chapter 16, the MIT Press, 1990
* [https://www.springer.com/engineering/circuits+%26+systems/book/978-0-387-35313-5 ''ए  Prए cticए l Introduction to PSL''], Cindy Eisner, Dए nए  Fismए n
* [https://www.springer.com/engineering/circuits+%26+systems/book/978-0-387-35313-5 ''A Practical Introduction to PSL''], Cindy Eisner, Dana Fisman
* {{cite book|editor1=Orna Grumberg|editor2=Helmut Veith|title=25 years of model checking: history, achievements, perspectives|year=2008|publisher=Springer|isbn=978-3-540-69849-4|chapter=From [[Alonzo Church|Church]] and Prior to [[Property Specification Language|PSL]]|first=Moshe Y. |last=Vardi|author-link=Moshe Vardi}} [http://www.cs.rice.edu/~vardi/papers/25mc.ps.gz preprint]. Historicए l perspective on how seemingly dispए rए te ideए s cए me together in computer science ए nd engineering. (The mention of Church in the title of this pए per is ए  reference to ए  little-known 1957 pए per, in which Church proposed ए  wए y to perform hए rdwए re verificए tion.)
* {{cite book|editor1=Orna Grumberg|editor2=Helmut Veith|title=25 years of model checking: history, achievements, perspectives|year=2008|publisher=Springer|isbn=978-3-540-69849-4|chapter=From [[Alonzo Church|Church]] and Prior to [[Property Specification Language|PSL]]|first=Moshe Y. |last=Vardi|author-link=Moshe Vardi}} [http://www.cs.rice.edu/~vardi/papers/25mc.ps.gz preprint]. Historical perspective on how seemingly disparate ideas came together in computer science and engineering. (The mention of Church in the title of this paper is a reference to a little-known 1957 paper, in which Church proposed a way to perform hardware verification.)
 
 
==अग्रिम पठन==
==अग्रिम पठन==
* {{cite book|author1=Peter Øhrstrøm|author2=Per F. V. Hasle|title=Temporal logic: from ancient ideas to artificial intelligence|year=1995|publisher=Springer|isbn=978-0-7923-3586-3}}
* {{cite book|author1=Peter Øhrstrøm|author2=Per F. V. Hasle|title=Temporal logic: from ancient ideas to artificial intelligence|year=1995|publisher=Springer|isbn=978-0-7923-3586-3}}
==बाहरी संबंध==
==बाहरी संबंध==
{{Commons category}}
*''[[Stanford Encyclopedia of Philosophy]]'': "[http://plato.stanford.edu/entries/logic-temporal/ Temporal Logic]"—by Anthony Galton.
*''[[Stanford Encyclopedia of Philosophy|Stए nford Encyclopediए  of Philosophy]]'': "[http://plato.stanford.edu/entries/logic-temporal/ Temporए l Logic]"—बीy ए nthony Gए lton.
*[http://staff.science.uva.nl/~yde/papers/TempLog.pdf ''Temporal Logic''] by Yde Venema, formal description of syntax and semantics, questions of axiomatization. Treating also Kamp's dyadic temporal operators (since, until)
*[http://staff.science.uva.nl/~yde/papers/TempLog.pdf ''Temporए l Logic''] बीy Yde Venemए , formए l description of syntए x ए nd semए ntics, questions of ए xiomए tizए tion. Treए ting ए lso Kए mp's dyए dic temporए l operए tors (since, until)
*[http://www.doc.ic.ac.uk/~imh/papers/sa.ps.gz Notes on games in temporal logic] by Ian Hodkinson, including a formal description of first-order temporal logic
*[http://www.doc.ic.ac.uk/~imh/papers/sa.ps.gz Notes on gए mes in temporए l logic] बीy Iए n Hodkinson, including ए  formए l description of first-order temporए l logic
*[http://cadp.inria.fr CADP – provides generic model checkers for various temporal logic]
*[http://cadp.inria.fr Cए DP – provides generic model checkers for vए rious temporए l logic]
*[http://www.comp.nus.edu.sg/~pat/ PAT] is a powerful free model checker, LTL checker, simulator and refinement checker for CSP and its extensions (with shared variable, arrays, wide range of fairness).
*[http://www.comp.nus.edu.sg/~pat/ Pए T] is ए  powerful free model checker, LTL checker, simulए tor ए nd refinement checker for CSP ए nd its extensions (with shए red vए riए बीle, ए rrए ys, wide rए nge of fए irness).
 
{{Non-classical logic}}
[[Category: लौकिक तर्क | लौकिक तर्क ]]
 
 


[[Category: Machine Translated Page]]
[[Category:CS1 English-language sources (en)]]
[[Category:Collapse templates]]
[[Category:Commons category link is the pagename]]
[[Category:Created On 02/03/2023]]
[[Category:Created On 02/03/2023]]
[[Category:Machine Translated Page]]
[[Category:Navigational boxes| ]]
[[Category:Navigational boxes without horizontal lists]]
[[Category:Pages with broken file links]]
[[Category:Pages with empty portal template]]
[[Category:Pages with reference errors]]
[[Category:Pages with script errors]]
[[Category:Portal templates with redlinked portals]]
[[Category:Templates Vigyan Ready]]

Latest revision as of 13:32, 29 August 2023

लॉजिक में, टेम्पोरल लॉजिक समय के संदर्भ में योग्य प्रस्तावों का प्रतिनिधित्व करने और उनके बारे में लॉजिक करने के लिए नियमों और प्रतीकों की कोई भी प्रणाली है (उदाहरण के लिए, मैं प्रायः भूखा हूं, मैं आखिरकार भूखा रहूंगा, या मैं भूखा रहूँगा जब तक मैं कुछ खा लूँगा )। यह कभी-कभी तनावपूर्ण लॉजिक को संदर्भित करने के लिए भी प्रयोग किया जाता है, 1950 के दशक के अंत में आर्थर प्रायर द्वारा प्रांरम्भ की गई टेम्पोरल लॉजिक की एक मॉडल लॉजिक-आधारित प्रणाली, उनका संघर्ष द्वारा महत्वपूर्ण योगदान के साथ। इसे कंप्यूटर वैज्ञानिकों, विशेष रूप से आमिर पनुएली और लॉजिकशास्त्रियों द्वारा विकसित किया गया है।

टेम्पोरल लॉजिक को औपचारिक सत्यापन में एक महत्वपूर्ण अनुप्रयोग मिला है, जहां इसका उपयोग हार्डवेयर या सॉफ्टवेयर सिस्टम की आवश्यकताओं को बताने के लिए किया जाता है। उदाहरण के लिए, कोई यह कहना चाह सकता है कि जब भी एक अनुरोध किया जाता है, संसाधन तक पहुंच आखिरकार दी जाती है, लेकिन यह दो अनुरोधकर्ताओं को एक साथ कभी नहीं दी जाती है। इस तरह के बयान को अस्थायी लॉजिक में आसानी से व्यक्त किया जा सकता है।

प्रेरणा

कथन पर विचार करें मुझे भूख लगी है। हालांकि इसका अर्थ समय में स्थिर है, कथन का सत्य मूल्य समय में भिन्न हो सकता है। कभी यह सच होता है, और कभी झूठ, लेकिन कभी भी सच और झूठ एक साथ नहीं। एक टेम्पोरल लॉजिक में, एक बयान में एक सत्य मूल्य हो सकता है जो समय के साथ बदलता रहता है - एक अस्थायी लॉजिक के विपरीत, जो केवल उन बयानों पर लागू होता है जिनके सत्य मूल्य समय में स्थिर होते हैं। समय के साथ सत्य-मूल्य का यह उपचार टेम्पोरल लॉजिक को कम्प्यूटेशनल क्रिया लॉजिक से अलग करता है।

टेम्पोरल लॉजिक में प्रायः टाइमलाइन के बारे में लॉजिक करने की क्षमता होती है। तथाकथित रैखिक-समय लॉजिक इस प्रकार के लॉजिक तक ही सीमित हैं। ब्रांचिंग-टाइम लॉजिक्स, हालांकि, कई समयसीमाओं के बारे में लॉजिक कर सकते हैं। यह उन वातावरणों के विशेष उपचार की अनुमति देता है जो अप्रत्याशित रूप से कार्य कर सकते हैं। उदाहरण को जारी रखने के लिए, ब्रांचिंग-टाइम लॉजिक में हम कह सकते हैं कि एक संभावना है कि मैं प्रायः के लिए भूखा रहूँगा, और एक संभावना है कि अंततः मुझे भूख नहीं लगेगी। यदि हम नहीं जानते कि मुझे कभी खिलाया जाएगा या नहीं, तो ये दोनों कथन सत्य हो सकते हैं।

इतिहास

हालांकि अरस्तू का लॉजिक लगभग पूरी तरह से स्पष्ट न्यायवाक्य के सिद्धांत से संबंधित है, उनके काम में ऐसे अंश हैं जिन्हें अब टेम्पोरल लॉजिक की प्रत्याशा के रूप में देखा जाता है, और प्रथम-क्रम लॉजिक का एक प्रारंभिक, आंशिक रूप से विकसित रूप हो सकता है। मोडल द्विसंयोजक लॉजिक लॉजिक। अरस्तू विशेष रूप से भविष्य की आकस्मिकताओं की समस्या से चिंतित था, जहां वह यह स्वीकार नहीं कर सकता था कि भविष्य की घटनाओं के बारे में बयानों पर द्वंद्व का सिद्धांत लागू होता है, यानी हम वर्तमान में यह तय कर सकते हैं कि भविष्य की घटनाओं के बारे में कोई बयान सही है या गलत, जैसे कि कल एक समुद्री युद्ध हो।[1] सहस्राब्दी के लिए बहुत कम विकास हुआ, चार्ल्स सैंडर्स पियर्स ने 19 वीं शताब्दी में उल्लेख किया:[2]

समय को सामान्यतः तर्कशास्त्रियों द्वारा 'एक्स्ट्रालॉजिकल' पदार्थ कहा जाता है। मैंने कभी इस राय को साझा नहीं किया। लेकिन मैंने सोचा है कि तर्क अभी तक विकास की स्थिति तक नहीं पहुंचा था, जिस पर इसके रूपों के लौकिक संशोधनों की प्रांरम्भ से बड़ी गड़बड़ी नहीं होगी; और मैं अभी भी उस तरह की सोच का हूं।

आश्चर्यजनक रूप से चार्ल्स सैंडर्स पियर्स के लिए, टेम्पोरल लॉजिक की पहली प्रणाली का निर्माण किया गया था, जहाँ तक हम जानते हैं, 20 वीं शताब्दी के पहले भाग में। हालांकि आर्थर प्रायर को व्यापक रूप से टेम्पोरल लॉजिक के संस्थापक के रूप में जाना जाता है, इस तरह के लॉजिक की पहली औपचारिकता 1947 में पोलिश लॉजिकशास्त्री जेरज़ी लोस द्वारा प्रदान की गई थी।[3] अपने काम पोडस्टावी एनालिज़ी मेटोडोलॉजिक्ज़नेज कानोनोव मिल्ला (द फाउंडेशन ऑफ़ ए मेथोडोलॉजिकल एनालिसिस ऑफ़ मिल्स मेथड्स) में उन्होंने मिल के सिद्धांतों का एक औपचारिक रूप प्रस्तुत किया। जेरज़ी लॉस के दृष्टिकोण में, समय कारक पर जोर दिया गया था। इस प्रकार, अपने लक्ष्य तक पहुँचने के लिए, उसे एक लॉजिक का निर्माण करना पड़ा जो लौकिक कार्यों की औपचारिकता के लिए साधन प्रदान कर सके। लॉजिक को जेरज़ी लॉस के मुख्य उद्देश्य के प्रतिफल के रूप में देखा जा सकता है,[4] यद्यपि यह पहला स्थितीय लॉजिक था, जिसे एक रूपरेखा के रूप में, बाद में ज्ञानशास्त्रीय लॉजिक में जेरज़ी लॉस के आविष्कारों के लिए इस्तेमाल किया गया था। लॉजिक में सिंटैक्स प्रायर के टेंस लॉजिक से बहुत अलग है, जो मोडल ऑपरेटरों का उपयोग करता है। जेरज़ी लॉस 'लॉजिक की भाषा बल्कि एक अहसास ऑपरेटर का उपयोग करती है, जो स्थिति संबंधी लॉजिक के लिए विशिष्ट है, जो विशिष्ट संदर्भ के साथ अभिव्यक्ति को बांधता है जिसमें इसका सत्य-मूल्य माना जाता है। जेरज़ी लॉस के कार्य में यह माना गया संदर्भ केवल लौकिक था, इस प्रकार अभिव्यक्ति विशिष्ट क्षणों या समय के अंतराल से बंधी हुई थी।

बाद के वर्षों में, आर्थर प्रायर द्वारा टेम्पोरल लॉजिकशास्त्र का शोध प्रांरम्भ हुआ।[4]वह स्वतंत्र इच्छा और पूर्वनियति के दार्शनिक निहितार्थों से चिंतित थे। उनकी पत्नी के अनुसार, उन्होंने पहली बार 1953 में टेम्पोरल लॉजिक को औपचारिक बनाने पर विचार किया। उनके शोध के परिणाम पहली बार 1954 में वेलिंग्टन में सम्मेलन में प्रस्तुत किए गए।[4]पहले प्रस्तुत की गई प्रणाली वाक्य रचना की दृष्टि से जेरज़ी लॉस लॉजिक के समान थी, हालांकि 1955 तक उन्होंने प्रायर के औपचारिक लॉजिक में परिशिष्ट 1 के अंतिम खंड में स्पष्ट रूप से जेरज़ी लॉस के कार्य का उल्लेख नहीं किया था।[4]

आर्थर प्रायर ने 1955-6 में ऑक्सफोर्ड विश्वविद्यालय में इस विषय पर व्याख्यान दिया, और 1957 में एक पुस्तक, टाइम एंड मॉडेलिटी प्रकाशित की, जिसमें उन्होंने दो लौकिक संयोजकों (मोडल ऑपरेटर्स ), एफ और पी के साथ एक प्रस्तावपरक लॉजिक मोडल लॉजिक पेश किया। भविष्य में कुछ समय और अतीत में कुछ समय के अनुरूप। इस प्रारंभिक कार्य में प्रायर ने समय को रेखीय माना। हालाँकि, 1958 में, उन्हें शाऊल क्रिपके का एक पत्र मिला, जिसने बताया कि यह धारणा शायद अनुचित है। एक ऐसे विकास में जिसने कंप्यूटर विज्ञान में इसी तरह के एक को पूर्वाभास दिया, प्रायर ने इसे सलाह के तहत लिया, और ब्रांचिंग टाइम के दो सिद्धांतों को विकसित किया, जिसे उन्होंने ओखमिस्ट और पीयरसियन कहा।[2], 1958 और 1965 के बीच प्रायर ने चार्ल्स लियोनार्ड हैम्बलिन के साथ भी पत्राचार किया था, और इस क्षेत्र में कई शुरुआती विकासों को इस पत्राचार से खोजा जा सकता है, उदाहरण के लिए हैम्ब्लिन निहितार्थ। प्रायर ने 1967 में इस विषय पर अपना सबसे परिपक्व काम पास्ट, प्रेजेंट, एंड फ्यूचर प्रकाशित किया। दो साल बाद उनकी मृत्यु हो गई।[5] तनावपूर्ण लॉजिक के साथ, आर्थर प्रायर ने स्थितीय लॉजिक की कुछ प्रणालियों का निर्माण किया, जो उनके मुख्य विचारों को जेर्जी लोश से विरासत में मिला।[6] 60 और 70 के दशक में निकोलस रेसचर द्वारा स्थितीय लौकिक लॉजिक्स में काम जारी रखा गया था। कालानुक्रमिक लॉजिक पर नोट (1966), कालानुक्रमिक प्रस्तावों के लॉजिक पर (1968), स्थलीय लॉजिक (1968), और टेम्पोरल लॉजिक (1971) जैसे कार्यों में उन्होंने जेरज़ी लॉस और आर्थर प्रायर की प्रणालियों के बीच संबंधों पर शोध किया। इसके अलावा उन्होंने साबित किया कि आर्थर प्रायर के काल संचालकों को विशिष्ट स्थितीय लॉजिकशास्त्र में एक अहसास संचालक का उपयोग करके परिभाषित किया जा सकता है।[6]निकोलस रेसचर ने अपने काम में, स्थितीय लॉजिकशास्त्र की अधिक सामान्य प्रणालियाँ भी बनाईं। हालांकि पहले वाले विशुद्ध रूप से लौकिक उपयोगों के लिए बनाए गए थे, उन्होंने लॉजिकशास्त्र के लिए टोपोलॉजिकल लॉजिक्स शब्द का प्रस्ताव दिया था, जो एक अहसास ऑपरेटर को सम्मिलित करने के लिए था, लेकिन कोई विशिष्ट लौकिक स्वयंसिद्ध नहीं था - जैसे घड़ी का स्वयंसिद्ध।

बाइनरी टेम्पोरल ऑपरेटर से और जब तक हंस काम्प द्वारा 1968 में अपनी पीएच.डी. में पेश किए गए थे। थीसिस,[7] जिसमें एक महत्वपूर्ण परिणाम भी सम्मिलित है जो टेम्पोरल लॉजिक को पहले क्रम के लॉजिक से संबंधित करता है - एक परिणाम जिसे अब काम्प के प्रमेय के रूप में जाना जाता है।[8][2][9] औपचारिक सत्यापन में दो प्रारंभिक दावेदार रैखिक टेम्पोरल लॉजिक थे, आमिर पनुएली द्वारा एक रैखिक-समय लॉजिक, और गणना वृक्ष लॉजिक (सीएलटी), मोर्दचाई बेन-अरी, जौहर मन्ना और अमीर पनुएली द्वारा एक शाखा-समय लॉजिक। लगभग उसी समय एडमंड एम. क्लार्क|ई द्वारा सीटीएल के लगभग समकक्ष औपचारिकता का सुझाव दिया गया था। एम. क्लार्क और ई. एलन एमर्सन|ई. ए एमर्सन। तथ्य यह है कि दूसरा लॉजिक पहले की तुलना में निर्णय समस्या कम्प्यूटेशनल जटिलता हो सकता है, सामान्य तौर पर ब्रांचिंग- और रैखिक-समय के लॉजिकों पर प्रतिबिंबित नहीं होता है, जैसा कि कभी-कभी लॉजिक दिया गया है। बदले में, इमर्सन और लेई दिखाते हैं कि किसी भी रैखिक-समय लॉजिक को शाखा-समय लॉजिक तक बढ़ाया जा सकता है जिसे उसी जटिलता से तय किया जा सकता है।

लॉस 'स्थितीय लॉजिक

जेरज़ी लॉस लॉजिक को उनके 1947 के मास्टर की थीसिस द फ़ाउंडेशन ऑफ़ ए मेथोडोलॉजिकल एनालिसिस ऑफ़ मिल्स मेथड्स के रूप में प्रकाशित किया गया था।[10] उनकी दार्शनिक और औपचारिक अवधारणाओं को लविव-वारसॉ स्कूल ऑफ़ लॉजिक की निरंतरता के रूप में देखा जा सकता है, क्योंकि उनके पर्यवेक्षक जेरज़ी स्लूपेकी थे, जो जन लुकासिविक्ज़ के शिष्य थे। पेपर का 1977 तक अंग्रेजी में अनुवाद नहीं किया गया था, हालांकि हेनरिक हाईज़ ने 1951 में एक संक्षिप्त, लेकिन सूचनात्मक, प्रतीकात्मक लॉजिक का जर्नल में समीक्षा प्रस्तुत की। इस समीक्षा में जेरज़ी लॉस के काम की मूल अवधारणाएँ सम्मिलित थीं और तार्किक समुदाय के बीच उनके परिणामों को लोकप्रिय बनाने के लिए पर्याप्त थीं। इस कार्य का मुख्य उद्देश्य मिल के सिद्धांतों को औपचारिक लॉजिक के ढांचे में प्रस्तुत करना था। इस लक्ष्य को प्राप्त करने के लिए लेखक ने मिल की अवधारणा की संरचना में लौकिक कार्यों के महत्व पर शोध किया। ऐसा करने के बाद, उन्होंने लॉजिक की अपनी स्वयंसिद्ध प्रणाली प्रदान की जो मिल के सिद्धांतों के साथ-साथ उनके लौकिक पहलुओं के लिए एक रूपरेखा के रूप में फिट होगी।

सिंटेक्स

पोडस्टावी एनालिज़ी मेटोडोलॉजिक्ज़नेज कानोनोव मिल्ला (द फ़ाउंडेशन ऑफ़ ए मेथोडोलॉजिकल एनालिसिस ऑफ़ मिल्स मेथड्स) में पहली बार प्रकाशित लॉजिक की भाषा में सम्मिलित हैं:[3]

  • पहले क्रम के लॉजिक ऑपरेटर्स '¬', '∧', '∨', '→', '≡', '∀' और '∃'
  • प्राप्ति संचालक U
  • कार्यात्मक प्रतीक δ
  • प्रस्तावक चर p1,p2,p3,...
  • समय के क्षणों को निरूपित करने वाले चर t1,t2,t3,...
  • समय अंतराल को निरूपित करने वाले चर n1,n2,n3,...

शर्तों का सेट (S द्वारा चिह्नित) निम्नानुसार बनाया गया है:

  • समय के क्षणों या अंतराल को दर्शाने वाले चर शब्द हैं
  • अगर और एक समय अंतराल चर है, तो

सूत्रों का सेट (जिसे फॉर द्वारा दर्शाया गया है) इस प्रकार बनाया गया है:

  • सभी प्रथम-क्रम लॉजिक सूत्र मान्य हैं
  • अगर और एक प्रस्तावक चर है, फिर
  • अगर , तब
  • अगर और , तब
  • अगर और और υ तब एक प्रस्तावात्मक, क्षण या अंतराल चर है







मूल स्वयंसिद्ध प्रणाली

पूर्व काल का लॉजिक (टीएल)

टाइम एंड मॉडेलिटी में पेश किए गए वाक्यात्मक काल लॉजिक में चार (गैर-सत्य कार्य | सत्य-कार्यात्मक) मोडल ऑपरेटर हैं (प्रस्तावात्मक कलन में सभी सामान्य सत्य-कार्यात्मक ऑपरेटरों के अलावा | प्रथम-क्रम प्रस्तावपरक लॉजिक)।[11]

  • P: यह मामला था कि... (P अतीत के लिए खड़ा है)
  • F: यह मामला होगा कि ... (F भविष्य के लिए खड़ा है)
  • G: प्रायः ऐसा ही रहेगा कि...
  • H: प्रायः ऐसा होता था कि...

इन्हें संयुक्त किया जा सकता है यदि हम π को एक अनंत पथ होने दें:[12]

  • : एक निश्चित बिंदु पर, पथ की सभी भावी अवस्थाओं में सत्य है
  • : पथ पर अपरिमित रूप से अनेक अवस्थाओं में सत्य है

P और F से G और H को परिभाषित किया जा सकता है, और इसके विपरीत:

सिंटेक्स और शब्दार्थ

टीएल के लिए एक न्यूनतम सिंटैक्स निम्नलिखित बैकस-नौर फॉर्म के साथ निर्दिष्ट किया गया है:

जहाँ ए कुछ परमाणु सूत्र है।[13] टीएल में वाक्य (गणितीय लॉजिक) की सच्चाई का मूल्यांकन करने के लिए कृपके शब्दार्थ का उपयोग किया जाता है। एक जोड़ी (T, <) एक सेट के T और एक द्विआधारी संबंध <पर T (प्राथमिकता कहा जाता है) को एक फ्रेम कहा जाता है। एक मॉडल ट्रिपल द्वारा दिया गया है (T, <, V) एक फ्रेम और एक फ़ंक्शन का V एक मूल्यांकन कहा जाता है जो प्रत्येक जोड़ी को निर्दिष्ट करता है (a, u) एक परमाणु सूत्र और एक समय मूल्य कुछ सत्य मान। धारणाϕ एक मॉडल में सच है U=(T, <, V) समय पर u संक्षिप्त है Uडबल घूमने वाला दरवाज़ा|⊨ϕ[u]। इस अंकन के साथ,[14]

कथन सच है जब बस
U⊨a[u] V(a,u)=true
U⊨¬ϕ[u] not U⊨ϕ[u]
U⊨(ϕ∧ψ)[u] U⊨ϕ[u] ए nd U⊨ψ[u]
U⊨(ϕ∨ψ)[u] U⊨ϕ[u] or U⊨ψ[u]
U⊨(ϕ→ψ)[u] U⊨ψ[u] if U⊨ϕ[u]
U⊨Gϕ[u] U⊨ϕ[v] for all v with u<v
U⊨Hϕ[u] U⊨ϕ[v] for all v with v<u

फ़्रेम के वर्ग F को देखते हुए, TL का एक वाक्य ϕ है

  • F के संबंध में वैध अगर प्रत्येक मॉडल U = (T, <, V) के साथ (T, <) F में और प्रत्येक u के लिए T में, U⊨ϕ [u]
  • F के संबंध में संतोषजनक अगर एक मॉडल U = (T, <, V) के साथ (T, <) F में ऐसा है कि T में कुछ u के लिए, U⊨ϕ [u]
  • F के संबंध में एक वाक्य ψ का परिणाम यदि प्रत्येक मॉडल के लिए U=(T,<,V) के साथ (T,<) F में और प्रत्येक u के लिए T में, यदि U⊨ψ[u], तो U⊨ϕ [u]

कई वाक्य केवल सीमित वर्ग के फ्रेम के लिए मान्य हैं। फ्रेम के वर्ग को उन लोगों तक सीमित करना आम है जिनके संबंध हैं < जो सकर्मक कमी, एंटीसिमेट्रिक संबंध , अल्हड़ रिलेशन, ट्राइकोटॉमी (गणित), अपरिवर्तनीय, कुल आदेश, घने क्रम, या इनमें से कुछ संयोजन है।

एक न्यूनतम स्वयंसिद्ध लॉजिक

बर्गेस एक ऐसे लॉजिक को रेखांकित करता है जो संबंध < पर कोई धारणा नहीं बनाता है, लेकिन निम्नलिखित स्वयंसिद्ध स्कीमा के आधार पर सार्थक कटौती की अनुमति देता है: [15]

  1. A जहां A प्रथम-क्रम लॉजिक का पुनरुत्पादन टॉटोलॉजी (लॉजिक)
  2. (A→B)→(GA→GB)
  3. H(A→B)→(HA→HB)
  4. A→GPA
  5. A→HFA

कटौती के निम्नलिखित नियमों के साथ:

  1. दिए गए A→B और A, घटाएँ B (एक वैध, सरल लॉजिक और निष्कर्ष के नियम के रूप)
  2. एक टॉटोलॉजी A दी गई, GA का अनुमान लगाएं
  3. एक टॉटोलॉजी A दिया, अनुमान हा

कोई निम्नलिखित नियम प्राप्त कर सकता है

  1. बेकर का नियम: दिया गया A→B, घटाएँ TA → TB जहां T एक काल है, G, H, F, और P से बना कोई भी अनुक्रमणिका।
  2. मिररिंग: एक प्रमेय दिया गया A, इसका दर्पण कथन निकालिए A§, जो G को H से (और इसलिए F को P से) और इसके विपरीत करके प्राप्त किया जाता है।
  3. द्वैत: एक प्रमेय दिया गया A, इसकी दोहरा कथन कथन A*, जो ∧ को ∨ से, G को F से, और H को P से धारणा प्राप्त की जाती है।

विधेय लॉजिक के लिए अनुवाद

बर्गेस टीएल में बयानों से एक मुक्त चर के साथ प्रथम-क्रम लॉजिक में बयानों में मेरेडिथ अनुवाद देता है x0 (वर्तमान क्षण का प्रतिनिधित्व)। यह अनुवाद M को पुनरावर्ती रूप से निम्नानुसार परिभाषित किया गया है:[15]

जहाँ वाक्य है सभी चर सूचकांकों के साथ 1 और की वृद्धि हुई द्वारा परिभाषित एक स्थान का विधेय है .

टेम्पोरल ऑपरेटर्स

टेम्पोरल लॉजिक में दो प्रकार के ऑपरेटर होते हैं: तार्किक ऑपरेटर और मोडल ऑपरेटर।[16] लॉजिकल ऑपरेटर सामान्य सत्य-कार्यात्मक ऑपरेटर होते हैं (). लीनियर टेम्पोरल लॉजिक और कम्प्यूटेशन ट्री लॉजिक में उपयोग किए जाने वाले मोडल ऑपरेटर्स को निम्नानुसार परिभाषित किया गया है।

शाब्दिक प्रतीकात्मक परिभाषा व्याख्या आरेख
बाइनरी ऑपरेटर्स
φ U ψ तब तक (Untill): ψ वर्तमान या भविष्य की स्थिति पर कायम रहता है, और φ को उस स्थिति तक बने रहना होता है। उस स्थिति में φ को और अधिक धारण करने की आवश्यकता नहीं है।
File:Timeline6.png
φ R ψ R elease: φ ψ जारी करता है यदि ψ सत्य है और इसमें पहली स्थिति सम्मिलित है जिसमें φ सत्य है (या हमेशा के लिए यदि ऐसी स्थिति सम्मिलित नहीं है)।
File:Timeline2.png
यूनरी ऑपरेटर्स
N φ N ext: φ को अगले राज्य में रखना है। ( एक्स समानार्थक रूप से प्रयोग किया जाता है।)
File:Timeline3.png
F φ Future : φ को अंततः पकड़ना होगा (कहीं बाद के रास्ते पर)।
File:Timeline4.png
G φ Globally: φ को बाद के पूरे रास्ते पर पकड़ बनानी है।
File:Timeline5-latest.png
A φ All: φ को वर्तमान स्थिति से प्रांरम्भ होने वाले सभी पथों पर पकड़ बनाना है।
E φ Exists: वर्तमान स्थिति से प्रारम्भ होने वाला कम से कम एक पथ सम्मिलित है जहां φ धारण करता है।

वैकल्पिक प्रतीक:

  • ऑपरेटर R को कभी-कभी V द्वारा निरूपित किया जाता है
  • ऑपरेटर W तक कमजोर ऑपरेटर है: के बराबर है

यूनरी ऑपरेटर जब भी अच्छी तरह से बने सूत्र होते हैं B(φ) सुगठित है। जब भी बाइनरी ऑपरेटर अच्छी तरह से गठित सूत्र होते हैं B(φ) और C(φ) सुगठित हैं।

कुछ लॉजिक्स में, कुछ ऑपरेटरों को व्यक्त नहीं किया जा सकता है। उदाहरण के लिए, एन ऑपरेटर को क्रियाओं के अस्थायी लॉजिक में व्यक्त नहीं किया जा सकता है।

टेम्पोरल लॉजिक्स

टेम्पोरल लॉजिक्स में सम्मिलित हैं:

लौकिक या कालानुक्रमिक या काल लॉजिक से निकटता से संबंधित भिन्नता, टोपोलॉजी, स्थान या स्थानिक स्थिति पर आधारित मोडल लॉजिक्स हैं।[22][23]

यह भी देखें

टिप्पणियाँ

  1. ↑ Vardi 2008, p. 153
  2. ↑ 2.0 2.1 2.2 Vardi 2008, p. 154
  3. ↑ 3.0 3.1 Łoś, Jerzy (1920-1998); Łoś, Jerzy (1920-1998) (1947). Podstawy analizy metodologicznej kanonów Milla. nakł. Uniwersytetu Marii Curie-Skłodowskiej.
  4. ↑ 4.0 4.1 4.2 4.3 Øhrstrøm, Peter (2019). "The Significance of the Contributions of A.N.Prior and Jerzy Łoś in the Early History of Modern Temporal Logic". Logic and Philosophy of Time: Further Themes from Prior, Volume 2 (in English).
  5. ↑ Peter Øhrstrøm; Per F. V. Hasle (1995). Temporal logic: from ancient ideas to artificial intelligence. Springer. ISBN 978-0-7923-3586-3. pp. 176–178, 210
  6. ↑ 6.0 6.1 Rescher, Nicholas; Garson, James (January 1969). "टोपोलॉजिकल लॉजिक". The Journal of Symbolic Logic (in English). 33 (4): 537–548. doi:10.2307/2271360. ISSN 0022-4812.
  7. ↑ "टेम्पोरल लॉजिक (स्टैनफोर्ड एनसाइक्लोपीडिया ऑफ फिलॉसफी)". Plato.stanford.edu. Retrieved 2014-07-30.
  8. ↑ Walter Carnielli; Claudio Pizzi (2008). तौर-तरीके और बहुविधता. Springer. p. 181. ISBN 978-1-4020-8589-5.
  9. ↑ Sergio Tessaris; Enrico Franconi; Thomas Eiter (2009). Reasoning Web. Semantic Technologies for Information Systems: 5th International Summer School 2009, Brixen-Bressanone, Italy, August 30 – September 4, 2009, Tutorial Lectures. Springer. p. 112. ISBN 978-3-642-03753-5.
  10. ↑ Tkaczyk, Marcin; Jarmużek, Tomasz (2019). "Jerzy Łoś Positional Calculus and the Origin of Temporal Logic". Logic and Logical Philosophy (in English). 28 (2): 259–276. doi:10.12775/LLP.2018.013. ISSN 2300-9802.
  11. ↑ Prior, Arthur Norman (2003). Time and modality: the John Locke lectures for 1955–6, delivered at the University of Oxford. Oxford: The Clarendon Press. ISBN 9780198241584. OCLC 905630146.
  12. ↑ Lawford, M. (2004). "टेम्पोरल लॉजिक्स का एक परिचय" (PDF). Department of Computer Science McMaster University.
  13. ↑ Goranko, Valentin; Galton, Antony (2015). Zalta, Edward N. (ed.). द स्टैनफोर्ड एनसाइक्लोपीडिया ऑफ फिलॉसफी (Winter 2015 ed.). Metaphysics Research Lab, Stanford University.
  14. ↑ Müller, Thomas (2011). "Tense or temporal logic" (PDF). In Horsten, Leon (ed.). दार्शनिक तर्क का सातत्य साथी. A&C Black. p. 329.
  15. ↑ Burgess, John P. (2009). दार्शनिक तर्क. Princeton, New Jersey: Princeton University Press. p. 17. ISBN 9781400830497. OCLC 777375659.
  16. ↑ "लौकिक तर्क". Stanford Encyclopedia of Philosophy. February 7, 2020. Retrieved April 19, 2022.
  17. ↑ 17.0 17.1 Maler, O.; Nickovic, D. (2004). "Monitoring temporal properties of continuous signals". doi:10.1007/978-3-540-30206-3_12.
  18. ↑ Mehrabian, Mohammadreza; Khayatian, Mohammad; Shrivastava, Aviral; Eidson, John C.; Derler, Patricia; Andrade, Hugo A.; Li-Baboud, Ya-Shian; Griffor, Edward; Weiss, Marc; Stanton, Kevin (2017). "साइबर-भौतिक प्रणालियों के समय के परीक्षण के लिए टाइमस्टैम्प टेम्पोरल लॉजिक (टीटीएल)।". ACM Transactions on Embedded Computing Systems. 16 (5s): 1–20. doi:10.1145/3126510. S2CID 3570088.
  19. ↑ Koymans, R. (1990). "Specifying real-time properties with metric temporal logic", Real-Time Systems 2(4): 255–299. doi:10.1007/BF01995674.
  20. ↑ Li, Xiao, Cristian-Ioan Vasile, and Calin Belta. "Reinforcement learning with temporal logic rewards." doi:10.1109/IROS.2017.8206234
  21. ↑ Clarkson, Michael R.; Finkbeiner, Bernd; Koleini, Masoud; Micinski, Kristopher K.; Rabe, Markus N.; Sánchez, César (2014). "Temporal Logics for Hyperproperties". सुरक्षा और विश्वास के सिद्धांत. Lecture Notes in Computer Science. Vol. 8414. pp. 265–284. doi:10.1007/978-3-642-54792-8_15. ISBN 978-3-642-54791-1. S2CID 8938993.
  22. ↑ Rescher, Nicholas (1968). "Topological Logic". दार्शनिक तर्क में विषय. pp. 229–249. doi:10.1007/978-94-017-3546-9_13. ISBN 978-90-481-8331-9.
  23. ↑ von Wright, Georg Henrik (1979). "A Modal Logic of Place". निकोलस रेस्चर का दर्शन. pp. 65–73. doi:10.1007/978-94-009-9407-2_9. ISBN 978-94-009-9409-6.

संदर्भ

अग्रिम पठन

  • Peter Øhrstrøm; Per F. V. Hasle (1995). Temporal logic: from ancient ideas to artificial intelligence. Springer. ISBN 978-0-7923-3586-3.

बाहरी संबंध

Retrieved from ‘https://www.vigyanwiki.in/index.php?title=टेम्पोरल_लॉजिक&oldid=254352’