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

摘要

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