टेम्पोरल लॉजिक: Difference between revisions
| Line 170: | Line 170: | ||
|'''तब''' तक (Untill): ψ वर्तमान या भविष्य की स्थिति पर कायम रहता है, और φ को उस स्थिति तक बने रहना होता है। उस स्थिति में φ को और अधिक धारण करने की आवश्यकता नहीं है। | |'''तब''' तक (Untill): ψ वर्तमान या भविष्य की स्थिति पर कायम रहता है, और φ को उस स्थिति तक बने रहना होता है। उस स्थिति में φ को और अधिक धारण करने की आवश्यकता नहीं है। | ||
|<timeline> | |<timeline> | ||
ImageSize = width:240 height:94 | |||
PlotArea = left:30 bottom:30 top:0 right:20 | |||
DateFormat = x.y | |||
Period = from:0 till:6 | Period = from:0 till:6 | ||
TimeAxis = orientation:horizontal | |||
AlignBars = justify | |||
ScaleMajor = gridcolor:black increment:1 start:0 | |||
ScaleMinor = gridcolor:black increment:1 start:0 | |||
PlotData= | |||
bar:p color:red width:10 align:left fontsize:S | |||
from:1 till:3 | from:1 till:3 | ||
bar:q color:red width:10 align:left fontsize:S | |||
from:3 till:5 | from:3 till:5 | ||
bar:pUq color:red width:10 align:left fontsize:S | |||
from:1 till:5 | from:1 till:5 | ||
</timeline> | </timeline> | ||
| Line 195: | Line 195: | ||
|'''R''' elease: φ ψ जारी करता है यदि ψ सत्य है और इसमें पहली स्थिति सम्मिलित है जिसमें φ सत्य है (या हमेशा के लिए यदि ऐसी स्थिति सम्मिलित नहीं है)। | |'''R''' elease: φ ψ जारी करता है यदि ψ सत्य है और इसमें पहली स्थिति सम्मिलित है जिसमें φ सत्य है (या हमेशा के लिए यदि ऐसी स्थिति सम्मिलित नहीं है)। | ||
|<timeline> | |<timeline> | ||
ImageSize = width:240 height:100 | |||
PlotArea = left:30 bottom:30 top:0 right:20 | |||
DateFormat = x.y | |||
Period = from:0 till:8 | Period = from:0 till:8 | ||
TimeAxis = orientation:horizontal | |||
AlignBars = justify | |||
ScaleMajor = gridcolor:black increment:1 start:0 | |||
ScaleMinor = gridcolor:black increment:1 start:0 | |||
PlotData= | |||
bar:p color:red width:10 align:left fontsize:S | |||
from:2 till:4 | from:2 till:4 | ||
from:6 till:8 | from:6 till:8 | ||
bar:q color:red width:10 align:left fontsize:S | |||
from:1 till:3 | from:1 till:3 | ||
from:5 till:6 | from:5 till:6 | ||
from:7 till:8 | from:7 till:8 | ||
bar:pRq color:red width:10 align:left fontsize:S | |||
from:1 till:3 | from:1 till:3 | ||
from:7 till:8 | from:7 till:8 | ||
| Line 226: | Line 226: | ||
|'''N''' ext: φ को अगले राज्य में रखना है। ( '''एक्स''' समानार्थक रूप से प्रयोग किया जाता है।) | |'''N''' ext: φ को अगले राज्य में रखना है। ( '''एक्स''' समानार्थक रूप से प्रयोग किया जाता है।) | ||
|<timeline> | |<timeline> | ||
ImageSize = width:240 height:60 | |||
PlotArea = left:30 bottom:30 top:0 right:20 | |||
DateFormat = x.y | |||
Period = from:0 till:6 | Period = from:0 till:6 | ||
TimeAxis = orientation:horizontal | |||
AlignBars = justify | |||
ScaleMajor = gridcolor:black increment:1 start:0 | |||
ScaleMinor = gridcolor:black increment:1 start:0 | |||
PlotData= | |||
bar:p color:red width:10 align:left fontsize:S | |||
from:2 till:3 | from:2 till:3 | ||
from:5 till:6 | from:5 till:6 | ||
bar:Np color:red width:10 align:left fontsize:S | |||
from:1 till:2 | from:1 till:2 | ||
from:4 till:5 | from:4 till:5 | ||
| Line 250: | Line 250: | ||
|'''Future''' : φ को अंततः पकड़ना होगा (कहीं बाद के रास्ते पर)। | |'''Future''' : φ को अंततः पकड़ना होगा (कहीं बाद के रास्ते पर)। | ||
|<timeline> | |<timeline> | ||
ImageSize = width:240 height:60 | |||
PlotArea = left:30 bottom:30 top:0 right:20 | |||
DateFormat = x.y | |||
Period = from:0 till:6 | Period = from:0 till:6 | ||
TimeAxis = orientation:horizontal | |||
AlignBars = justify | |||
ScaleMajor = gridcolor:black increment:1 start:0 | |||
ScaleMinor = gridcolor:black increment:1 start:0 | |||
PlotData= | |||
bar:p color:red width:10 align:left fontsize:S | |||
from:2 till:3 | from:2 till:3 | ||
from:4 till:5 | from:4 till:5 | ||
bar:Fp color:red width:10 align:left fontsize:S | |||
from:0 till:5 | from:0 till:5 | ||
</timeline> | </timeline> | ||
| Line 273: | Line 273: | ||
|'''G'''lobally: φ को बाद के पूरे रास्ते पर पकड़ बनानी है। | |'''G'''lobally: φ को बाद के पूरे रास्ते पर पकड़ बनानी है। | ||
|<timeline> | |<timeline> | ||
ImageSize = width:240 height:60 | |||
PlotArea = left:30 bottom:30 top:0 right:20 | |||
DateFormat = x.y | |||
Period = from:0 till:6 | Period = from:0 till:6 | ||
TimeAxis = orientation:horizontal | |||
AlignBars = justify | |||
ScaleMajor = gridcolor:black increment:1 start:0 | |||
ScaleMinor = gridcolor:black increment:1 start:0 | |||
PlotData= | |||
bar:p color:red width:10 align:left fontsize:S | |||
from:1 till:3 | from:1 till:3 | ||
from:4 till:6 | from:4 till:6 | ||
bar:Gp color:red width:10 align:left fontsize:S | |||
from:4 till:6 | from:4 till:6 | ||
</timeline> | </timeline> | ||
| Line 310: | Line 310: | ||
कुछ लॉजिक्स में, कुछ ऑपरेटरों को व्यक्त नहीं किया जा सकता है। उदाहरण के लिए, एन ऑपरेटर को क्रियाओं के अस्थायी लॉजिक में व्यक्त नहीं किया जा सकता है। | कुछ लॉजिक्स में, कुछ ऑपरेटरों को व्यक्त नहीं किया जा सकता है। उदाहरण के लिए, एन ऑपरेटर को क्रियाओं के अस्थायी लॉजिक में व्यक्त नहीं किया जा सकता है। | ||
[[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 empty portal template]] | |||
[[Category:Pages with reference errors]] | |||
[[Category:Pages with script errors]] | |||
[[Category:Portal templates with redlinked portals]] | |||
== टेम्पोरल लॉजिक्स == | == टेम्पोरल लॉजिक्स == | ||
Revision as of 12:59, 20 March 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 के मास्टर की थीसिस द फ़ाउंडेशन ऑफ़ ए मेथोडोलॉजिकल एनालिसिस ऑफ़ मिल्स मेथड्स के रूप में प्रकाशित किया गया था।Cite error: Invalid <ref> tag; invalid names, e.g. too many उनकी दार्शनिक और औपचारिक अवधारणाओं को लविव-वारसॉ स्कूल ऑफ़ लॉजिक की निरंतरता के रूप में देखा जा सकता है, क्योंकि उनके पर्यवेक्षक जेरज़ी स्लूपेकी थे, जो जन लुकासिविक्ज़ के शिष्य थे। पेपर का 1977 तक अंग्रेजी में अनुवाद नहीं किया गया था, हालांकि हेनरिक हाईज़ ने 1951 में एक संक्षिप्त, लेकिन सूचनात्मक, प्रतीकात्मक लॉजिक का जर्नल में समीक्षा प्रस्तुत की। इस समीक्षा में जेरज़ी लॉस के काम की मूल अवधारणाएँ सम्मिलित थीं और तार्किक समुदाय के बीच उनके परिणामों को लोकप्रिय बनाने के लिए पर्याप्त थीं। इस कार्य का मुख्य उद्देश्य मिल के सिद्धांतों को औपचारिक लॉजिक के ढांचे में प्रस्तुत करना था। इस लक्ष्य को प्राप्त करने के लिए लेखक ने मिल की अवधारणा की संरचना में लौकिक कार्यों के महत्व पर शोध किया। ऐसा करने के बाद, उन्होंने लॉजिक की अपनी स्वयंसिद्ध प्रणाली प्रदान की जो मिल के सिद्धांतों के साथ-साथ उनके लौकिक पहलुओं के लिए एक रूपरेखा के रूप में फिट होगी।
सिंटेक्स
पोडस्टावी एनालिज़ी मेटोडोलॉजिक्ज़नेज कानोनोव मिल्ला (द फ़ाउंडेशन ऑफ़ ए मेथोडोलॉजिकल एनालिसिस ऑफ़ मिल्स मेथड्स) में पहली बार प्रकाशित लॉजिक की भाषा में सम्मिलित हैं:[3]
- पहले क्रम के लॉजिक ऑपरेटर्स '¬', '∧', '∨', '→', '≡', '∀' और '∃'
- प्राप्ति संचालक U
- कार्यात्मक प्रतीक δ
- प्रस्तावक चर p1,p2,p3,...
- समय के क्षणों को निरूपित करने वाले चर t1,t2,t3,...
- समय अंतराल को निरूपित करने वाले चर n1,n2,n3,...
शर्तों का सेट (S द्वारा चिह्नित) निम्नानुसार बनाया गया है:
- समय के क्षणों या अंतराल को दर्शाने वाले चर शब्द हैं
- अगर और एक समय अंतराल चर है, तो
सूत्रों का सेट (जिसे फॉर द्वारा दर्शाया गया है) इस प्रकार बनाया गया है:Cite error: Invalid <ref> tag; invalid names, e.g. too many
- सभी प्रथम-क्रम लॉजिक सूत्र मान्य हैं
- अगर और एक प्रस्तावक चर है, फिर
- अगर , तब