घटना गणना

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

स्पष्टता और घटना

घटना की गणना में, स्पष्ट पुनःकरण हैं। इसका अर्थ यह है कि उन्हें विधेय के माध्यम से नहीं बल्कि फलन के माध्यम से औपचारिक रूप दिया जाता है। एक अलग विधेय होल्ड्सएट का उपयोग यह बताने के लिए किया जाता है कि कौनसी स्पष्टता किसी निश्चित समय बिंदु पर उपलब्ध हैं। उदाहरण के लिए, ${\mathit {HoldsAt}}(on(box,table),t)$ इसका अर्थ है कि t समय पर बॉक्स मेज पर है; इस सूत्र में, होल्ड्सएट एक विधेय है और ऑन एक फलन है।

घटनाओं को पदों के रूप में भी दर्शाया जाता है। घटनाओं का प्रभाव विधेय, आरंभ और समाप्ति का उपयोग करके दिया जाता है। विशेष रूप से, ${\mathit {Initiates}}(e,f,t)$ का अर्थ है कि, यदि घटना को e पद द्वारा t समय पर निष्पादित किया जाता है तो t समय पर स्पष्टता f सत्य होगी। समाप्ति विधेय का अर्थ आरंभ विधेय के समतुल्य ही होता है, केवल अंतर के साथ कि t समय पर स्पष्टता f असत्य होगी।

कार्यक्षेत्र-स्वतंत्र सिद्धांत

क्रियाओं का प्रतिनिधित्व करने के लिए अन्य भाषाओं की तरह, घटना की गणना एक स्वेच्छ क्रिया के बाद प्रत्येक स्पष्टता के मान को बताने वाले सूत्रों के माध्यम से स्पष्टता के सही विकास को औपचारिक बनाता है। घटना की गणना तंत्र समस्या को इस तरह से हल करता है जो स्थिति गणना के अनुक्रमित अवस्था सिद्धांत के समतुल्य है: t समय पर स्पष्टता सत्य होती है यदि और केवल यदि इसे अतीत में सत्य बनाया गया हो और इस बीच असत्य नहीं बनाया गया हो।

${\mathit {HoldsAt}}(f,t)\leftarrow [{\mathit {Happens}}(e,t_{1})\wedge {\mathit {Initiates}}(e,f,t_{1})\wedge (t_{1}<t)\wedge \neg {\mathit {Clipped}}(t_{1},f,t)]$

इस सूत्र का अर्थ है कि t समय पर f पद द्वारा दर्शायी गयी स्पष्टता सत्य है अगर:

1. ${\mathit {Happens}}(e,t_{1})$; एक घटना e घटित हुआ था,
2. ${\mathit {t}}_{1}<t$; यह अतीत में हुआ था:
3. ${\mathit {Initiates}}(e,f,t_{1})$; इस घटना में प्रभाव के रूप में f स्पष्टता है,
4. ${\mathit {Clipped}}(t_{1},f,t)$; इस बीच स्पष्टता को असत्य नहीं बनाया गया है

एक समतुल्य सूत्र का उपयोग विपरीत स्थितियों को औपचारिक बनाने के लिए किया जाता है जिसमें एक निश्चित समय पर स्पष्टता असत्य होती है। किसी घटना की के प्रभावित होने से पहले स्पष्टता को उचित तरीके से औपचारिक बनाने के लिए अन्य सूत्रों की भी आवश्यकता होती है। ये सूत्र उपरोक्त के समतुल्य हैं, लेकिन ${\mathit {Happens}}(e,t_{1})\wedge {\mathit {Initiates}}(e,f,t_{1})$ को ${\mathit {HoldsAt}}(f,t_{1})$ द्वारा प्रतिस्थापित किया गया है।

क्लिप्ड विधेय, जिसमें कहा गया है कि एक अंतराल के दौरान स्पष्टता को असत्य बना दिया जाता है, इसे स्वयंसिद्ध किया जा सकता है या बस संकेतलिपि के रूप में लिया जा सकता है, इस प्रकार:

$\mathit{C}\mathit{l}\mathit{i}\mathit{p}\mathit{p}\mathit{e}\mathit{d}(t_1,f,t_{}$