基于动态时序描述逻辑的动作理论

动态时序描述逻辑(dltldl)是一类描述逻辑的动态时序扩展。提出一种基于dltlalcio的动态域建模方法,利用该方法可构造出刻画动态域知识的dltlalcio理论,并解决动作推理中的框架问题和分支问题。动作推理问题,如动作可执行性和投影问题等,可归结为关于dltlalcio理论的推理问题,并最终归结为dltlalcio的公式可满足性问题。dltlalcio公式可表达动作和时间约束,相对于其他基于描述逻辑的动作形式,基于dltlalcio的动作形式在需要执行复杂查询,尤其是含时间或动作的查询的应用场合具有更好的适用性。