人工智能规划(AI planning)是人工智能领域的一个重要研究方向,它主要研究智能主体在给定一系列关于动作的描述的前提下,如何生成一个规划(plan)以完成被赋予的任务或目标。为了更好地进行规划,我们需要研究动作能够执行的前提和其产生的效果,以及其效果对世界状态和主体的认知状态的影响,这属于动作推理的范畴,是人工智能规划的一个分支。对动作推理的研究,有助于我们预测某一个动作序列所产生的最终效果,以及验证其能否实现目标,从而帮助我们更好地提出一个可行规划。相对于传统的完全信息的序列规划(规划是一个动作序列),不完全信息下的循环规划(带有循环结构的规划)因更具一般性和简洁性,而受到越来越多的关注。尽管已有许多学者对带循环的规划问题的算法方面进行研究,然而其语义方面却没有得到足够的重视,大量例子表明,程序语言的形式语义也是非常重要的。本文在综合考虑和比较动作推理的主要逻辑表达方式后,决定采用具有类似于自然语言语法的动作语言来研究动作推理的性质以及相关问题,以两个例子作为动机,将感知动作、非确定动作和循环在动作语言中结合,得到动作语言ALK以处理在非确定论域下带循环的规划问题,然后给出AL K的两个基于转移系统的形式语义——通用语义和0-逼近语义。接着,基于0-逼近语义,我们为AL K构造一个可靠且(相对)完全的霍尔证明系统,用于规划的生成和验证。该系统使用了知识编译中的离线编译和在线推理的思想,使得智能主体能够利用空闲的时间和空间,尽可能多地验证相对较短的规划,然后使用系统中的组合性规则将这些已验证的规划组合成较长的规划,以完成快速的在线回答。换句话说,智能主体可以利用已有的规划生成和验证新的规划,从而大大提高实际规划的效率。我们认为,本文构建的形式语义以及证明系统均可作为带循环的动作推理的逻辑基础。