लौकिक तर्क

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

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

प्रेरणा

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

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

इतिहास

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

Time has usually been considered by logicians to be what is called 'extralogical' matter. I have never shared this opinion. But I have thought that logic had not yet reached the state of development at which the introduction of temporal modifications of its forms would not result in great confusion; and I am much of that way of thinking yet.

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

बाद के वर्षों में, आर्थर प्रायर द्वारा लौकिक तर्कशास्त्र का शोध शुरू हुआ।वह स्वतंत्र इच्छा और पूर्वनियति के दार्शनिक निहितार्थों से चिंतित थे। उनकी पत्नी के अनुसार, उन्होंने पहली बार 1953 में लौकिक तर्क को औपचारिक बनाने पर विचार किया। उनके शोध के परिणाम पहली बार 1954 में वेलिंग्टन में सम्मेलन में प्रस्तुत किए गए।पहले प्रस्तुत की गई प्रणाली वाक्यात्मक रूप से जेरज़ी Łoś|Łoś' तर्क के समान थी, हालांकि 1955 तक उन्होंने प्रायर के औपचारिक तर्क में परिशिष्ट 1 के अंतिम खंड में स्पष्ट रूप से Jerzy Łoś|Łoś' कार्य का उल्लेख नहीं किया था।

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

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

मूस 'स्थितीय तर्क

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

सिंटेक्स

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

• पहले क्रम के लॉजिक ऑपरेटर्स '¬', '∧', '∨', '→', '≡', '∀' और '∃'
• प्राप्ति संचालक यू
• कार्यात्मक प्रतीक δ
• प्रस्तावक चर पी₁,पी₂,पी₃,...
• समय के क्षणों को निरूपित करने वाले चर टी₁,टी₂,टी₃,...
• समय अंतराल n को निरूपित करने वाले चर₁,एन₂,एन₃,...

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

• समय के क्षणों या अंतराल को दर्शाने वाले चर शब्द हैं
• अगर $\tau \in S$ और $\epsilon$ एक समय अंतराल चर है, तो $\delta (\tau ,\epsilon )\in S$

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

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

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

1. $U_{t_{1}}\neg p_{1}\equiv \neg U_{t_{1}}p_{1}$
2. $U_{t_{1}}(p_{1}\rightarrow p_{2})\rightarrow (U_{t_{1}}p_{1}\rightarrow U_{t_{1}}p_{2})$
3. $U_{t_{1}}((p_{1}\rightarrow p_{2})\rightarrow ((p_{2}\rightarrow p_{3})\rightarrow (p_{1}\rightarrow p_{3})))$
4. $U_{t_{1}}(p_{1}\rightarrow (\neg p_{1}\rightarrow p_{2}))$
5. $U_{t_{1}}((\neg p_{1}\rightarrow p_{1})\rightarrow p_{1})$
6. $\forall _{t_{1}}U_{t_{1}}p_{1}\rightarrow p_{1}$
7. $\forall _{t_{1}}\forall _{n_{1}}\exists _{t_{2}}\forall _{p_{1}}(U_{\delta (t_{1},n_{1})}p_{1}\equiv U_{t_{2}}p_{1})$
8. $\forall _{t_{1}}\forall _{n_{1}}\exists _{t_{2}}\forall _{p_{1}}(U_{\delta (t_{2},n_{1})}p_{1}\equiv U_{t_{1}}p_{1})$
9. $\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}))$

पूर्व काल का तर्क (टीएल)

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

• पी: यह मामला था कि... (पी अतीत के लिए खड़ा है)
• एफ: यह मामला होगा कि ... (एफ भविष्य के लिए खड़ा है)
• जी: हमेशा ऐसा ही रहेगा कि...
• एच: हमेशा ऐसा होता था कि...

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

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

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

${\begin{aligned}F&\equiv \lnot G\lnot \\P&\equiv \lnot H\lnot \end{aligned}}$

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

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

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

Statement	... is true just when
U⊨a[u]	V(a,u)=true
U⊨¬ϕ[u]	not U⊨ϕ[u]
U⊨(ϕ∧ψ)[u]	U⊨ϕ[u] and 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

एक वर्ग दिया {{var|F}फ्रेम के }, एक वाक्य {{var|ϕ}टीएल का है

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

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

एक न्यूनतम स्वयंसिद्ध तर्क

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

1. A कहाँ A प्रथम-क्रम तर्क का एक टॉटोलॉजी (तर्क) है
2. जी(A→B)→(जीA→GB)
3. एच(A→B)→(एचA→HB)
4. A→GPA
5. A→HFA

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

1. दिया गया A→B और A, निकालिए B (सेटिंग मोड)
2. एक तनातनी दी A, अनुमान जीA
3. एक तनातनी दी A, अनुमान एचA

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

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

विधेय तर्क के लिए अनुवाद

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

${\begin{aligned}&M(a)&&=a^{*}x_{0}\\&M(\lnot \phi )&&=\lnot M(\phi )\\&M(\phi \land \psi )&&=M(\phi )\land M(\psi )\\&M({\mathsf {G}}\phi )&&=\forall x_{1}(x_{0}<x_{1}\rightarrow M(A^{+}))\\&M({\mathsf {H}}\phi )&&=\forall x_{1}(x_{1}<x_{0}\rightarrow M(A^{+}))\end{aligned}}$ कहाँ $A^{+}$ वाक्य है $A$ सभी चर सूचकांकों के साथ 1 और की वृद्धि हुई $a^{*}$ द्वारा परिभाषित एक स्थान का विधेय है $x\mapsto V(a,x)$.

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

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

Textual	Symbolic	Definition	Explanation	Diagram
Binary operators
φ U ψ	$\phi ~{\mathcal {U}}~\psi$	$(B\,{\mathcal {U}}\,C)(\phi )=\ (\exists i:C(\phi _{i})\land (\forall j<i:B(\phi _{j})))$	Until: ψ holds at the current or a future position, and φ has to hold until that position. At that position φ does not have to hold any more.	<timeline> ImageSize = width:240 height:94 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y 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 bar:q color:red width:10 align:left fontsize:S from:3 till:5 bar:pUq color:red width:10 align:left fontsize:S from:1 till:5 </timeline>
φ R ψ	$\phi ~{\mathcal {R}}~\psi$	$(B\,{\mathcal {R}}\,C)(\phi )=\ (\forall i:C(\phi _{i})\lor (\exists j<i:B(\phi _{j})))$	Release: φ releases ψ if ψ is true up until and including the first position in which φ is true (or forever if such a position does not exist).	<timeline> ImageSize = width:240 height:100 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y 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:6 till:8 bar:q color:red width:10 align:left fontsize:S from:1 till:3 from:5 till:6 from:7 till:8 bar:pRq color:red width:10 align:left fontsize:S from:1 till:3 from:7 till:8 </timeline>
Unary operators
N φ	$\bigcirc \phi$	${\mathcal {N}}B(\phi _{i})=B(\phi _{i+1})$	Next: φ has to hold at the next state. (X is used synonymously.)	<timeline> ImageSize = width:240 height:60 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y 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:5 till:6 bar:Np color:red width:10 align:left fontsize:S from:1 till:2 from:4 till:5 </timeline>
F φ	$\Diamond \phi$	${\mathcal {F}}B(\phi )=(true\,{\mathcal {U}}\,B)(\phi )$	Future: φ eventually has to hold (somewhere on the subsequent path).	<timeline> ImageSize = width:240 height:60 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y 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:4 till:5 bar:Fp color:red width:10 align:left fontsize:S from:0 till:5 </timeline>
G φ	$\Box \phi$	${\mathcal {G}}B(\phi )=\neg {\mathcal {F}}\neg B(\phi )$	Globally: φ has to hold on the entire subsequent path.	<timeline> ImageSize = width:240 height:60 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y 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:4 till:6 bar:Gp color:red width:10 align:left fontsize:S from:4 till:6 </timeline>
A φ	$\forall \phi$	$({\mathcal {A}}B)(\psi )=\ (\forall \phi :\phi _{0}=\psi \to B(\phi ))$	All: φ has to hold on all paths starting from the current state.
E φ	$\exists \phi$	$({\mathcal {E}}B)(\psi )=\ (\exists \phi :\phi _{0}=\psi \land B(\phi ))$	Exists: there exists at least one path starting from the current state where φ holds.

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

• ऑपरेटर आर को कभी-कभी वी द्वारा निरूपित किया जाता है
• ऑपरेटर W तक कमजोर ऑपरेटर है: $f\mathbf {W} g$ के बराबर है $f\mathbf {U} g\lor \mathbf {G} f$

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

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

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

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

• स्थितीय तर्क की कुछ प्रणालियाँ
• लीनियर टेम्पोरल लॉजिक (LTLअंतराल लौकिक तर्क बिना ब्रांचिंग टाइमलाइन के
• कम्प्यूटेशन ट्री लॉजिक (CTL) टेम्पोरल लॉजिक ब्रांचिंग टाइमलाइन के साथ
• अंतराल अस्थायी तर्क (आईटीएल)
• कार्यों का अस्थायी तर्क (टीएलए)
• सिग्नल टेम्पोरल लॉजिक (STL)* टाइमस्टैम्प अस्थायी तर्क (TTL)
• संपत्ति विशिष्टता भाषा (पीएसएल)
• सीटीएल*, जो एलटीएल और सीटीएल का सामान्यीकरण करता है
• हेनेसी-मिलनर लॉजिक (HML)
• मोडल μ-कैलकुलस, जिसमें एक सबसेट HML और CTL के रूप में शामिल है*
• मीट्रिक लौकिक तर्क (MTL)
• मीट्रिक अंतराल लौकिक तर्क (MITL)
• समयबद्ध प्रस्तावपरक लौकिक तर्क (TPTL)
• ट्रंकेटेड लीनियर टेम्पोरल लॉजिक (TLTL)
• हाइपर टेम्पोरल लॉजिक (हाइपरएलटीएल)

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

यह भी देखें

• एचपीओ औपचारिकता
• कृपके संरचना
• ऑटोमेटा सिद्धांत
• चॉम्स्की व्याकरण
• राज्य संक्रमण प्रणाली
• अवधि कलन (डीसी)
• हाइब्रिड तर्क
• परिमित-राज्य सत्यापन में अस्थायी तर्क
• Reo समन्वय भाषा
• मोडल लॉजिक
• अनुसंधान सामग्री: मैक्स प्लैंक सोसायटी आर्काइव

संदर्भ

• Mordechai Ben-Ari, Zohar Manna, Amir Pnueli: The Temporal Logic of Branching Time. POPL 1981: 164–176
• Amir Pnueli: The Temporal Logic of Programs FOCS 1977: 46–57
• Venema, Yde, 2001, "Temporal Logic," in Goble, Lou, ed., The Blackwell Guide to Philosophical Logic. Blackwell.
• E. A. Emerson and Chin-Laung Lei, "Modalities for model checking: branching time logic strikes back", in Science of Computer Programming 8, pp. 275–306, 1987.
• E. A. Emerson, "Temporal and modal logic", Handbook of Theoretical Computer Science, Chapter 16, the MIT Press, 1990
• A Practical Introduction to PSL, Cindy Eisner, Dana Fisman
• Vardi, Moshe Y. (2008). "From Church and Prior to PSL". In Orna Grumberg; Helmut Veith (eds.). 25 years of model checking: history, achievements, perspectives. Springer. ISBN 978-3-540-69849-4. 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.)

अग्रिम पठन

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

बाहरी संबंध

• Stanford Encyclopedia of Philosophy: "Temporal Logic"—by Anthony Galton.
• Temporal Logic by Yde Venema, formal description of syntax and semantics, questions of axiomatization. Treating also Kamp's dyadic temporal operators (since, until)
• Notes on games in temporal logic by Ian Hodkinson, including a formal description of first-order temporal logic
• CADP – provides generic model checkers for various temporal logic
• 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).