摘要：经典智能规划问题是人工智能研究领域里最为重要的问题之一。但是由于其时间复杂度上的不可跟踪性,使得这项技术在实际应用中的范围十分受限,所以一直以来,与智能规划有关的计算复杂性问题备受关注。本文试图从形式描述的角度探究智能规划的计算复杂性。本文提出一种全新的方法：使用形式逻辑语言来描述经典智能规划问题,并提供相应的算法来将这种描述“解释”为传统的基于动作的规划问题描述。在本文的算法之前,还没有能够完全实现该功能的方法,达到使任何一种泛化描述的PSPACE类问题转化为基于动作的智能规划问题。该方法是基于二阶传递闭包逻辑(SO(TC))的。首先,本文提出一种SO(TC)的范式,并证明其完全性,根据这个证明,可以容易的得到一种可以针对SO(TC)范围内的任何表达式的规范化方法。在此基础上,提出一个算法,可以直接将这种范式“解释”成一个PDDL语言描述的智能规划问题,于是就得到了一个完整的算法。生成结果编码使用PDDL这种功能丰富的语言。本问提出的这个方法,价值可以体现在两个方面：一方面,这个算法使得使用智能规划求解器来求解逻辑化描述的模型检测问题成为可能。这种逻辑描述,既可以来自手工编制的代码,也可以由其它形式描述转化而来；另一方面,本文提出的这种二阶逻辑的传递闭包范式,可以看成是一种紧凑的,统一的智能规划问题描述,本文认为这种描述方法可以促进智能规划理论的进一步研究。该算法由两个主要过程连接组成。本文使用C++编程语言实现了这个算法,该程序能够生成标准的PDDL代码,可以直接作为智能规划求解器的输入数据,进行求解。最后,我们证明本算法的一条重要性质,能够保证在转化的过程中不扩大NP的复杂度。