事件微積分
編輯事件微積分是一種用于表示和推理事件及其影響的邏輯語言,由RobertKowalski和MarekSergot于1986年首次提出。它在20世紀90年代被MurrayShanahan和RobMiller擴展。與其他用于推理變化的語言類似,事件微積分表示行動對流體的影響。然而,事件也可以是系統外部的。在事件微積分中,人們可以指定通量在某些給定時間點的值,在給定時間點發生的事件,以及它們的影響。
通量和事件
編輯在事件微積分中,通量是被重構的。這意味著它們不是通過謂詞而是通過函數來形式化的。一個單獨的謂詞HoldsAt被用來告訴哪些通量在給定的時間點上保持。比如說。表示盒子在時間t在桌子上;在這個公式中,HoldsAt是一個謂詞,而on是一個函數。事件也被表示為術語。事件的效果用謂詞Initiates和Terminates給出。特別是。發起(Initiates(e,f,t){displaystyle{mathit{Initiates}}(e,f,t)}意味著,如果術語e所代表的事件在時間t被執行,那么f在t之后將為真。Terminates謂詞有類似的含義,xxx的區別是f在t之后將為假。
與領域無關的公理
編輯像其他表示動作的語言一樣,事件微積分通過告訴任意動作執行后每個通感的值的公式來形式化通感的正確演變。事件微積分解決框架問題的方式類似于情境微積分的繼任狀態公理:當且僅當一個通感在過去被變成了真,并且在此期間沒有被變成假時,它在時間t是真的。這個公式的意思是,術語f所代表的流變在時間t是真的,如果。一個類似的公式被用來正式化相反的情況,即一個通證在給定時間是假的。還需要其他公式來正確地形式化在事件影響之前的通證。這些公式與上述公式類似,但是Clipped謂詞,說明在一個區間內,一個流變被弄成了假的,可以被公理化,或者簡單地作為一個縮寫,如下。
依賴于領域的公理
編輯上面的公理與謂詞HoldsAt、Initiates和Terminates的值有關,但沒有說明哪些通證是已知的,哪些事件實際上使通證為真或假。這是通過使用一組依賴領域的公理來實現的。通量的已知值被表述為簡單的字詞.事件的效果是由事件的效果與它們的前提條件相關的公式來說明的。例如,如果事件open使流暢isopen為真,但只有當haskey當前為真時,事件微積分中的相應公式為。這個等價關系的右側表達式是由一個二項式組成的:對于每個事件和可以由事件變成真實的流暢,有一個二項式說e實際上是那個事件,f實際上是那個流暢,而且事件的前提條件得到滿足。
內容由匿名用戶提供,本內容不代表www.gelinmeiz.com立場,內容投訴舉報請聯系www.gelinmeiz.com客服。如若轉載,請注明出處:http://www.gelinmeiz.com/167710/