事件微积分

事件微积分是一种用于表示和推理事件及其影响的逻辑语言，由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实际上是那个流畅，而且事件的前提条件得到满足。