智能规划(Intelligent Planning)是人工智能一个重要的研究方向,求解规划的方法很多,其中一种方法就是将规划问题转化成量化布尔范式进行求解。自动推理是人工智能研究领域最重要的研究方向之一,知识编译(Knowledge Compilation)是近年来提出的卓有成效的推理问题处理方法之一。目前大多数知识编译方法都是基于命题逻辑的。量化布尔范式(Quantified Boolean Formulae,QBF)是人工智能的一个重要研究方向。QBF是一种具有量词前缀的命题逻辑公式,该公式中的变量都是由存在量词或者全称量词限制。虽然判断QBF问题的可满足性的计算复杂性是PSPACE完备的,但是QBF比命题逻辑更富有表达能力,因此QBF的许多子类都可以作为知识编译的目标语言。本文将命题知识编译方法扩展到QBF中,提出了QBF的近似知识编译方法。该方法选择QBF的子类QHorn理论作为知识编译的目标语言。本文首先定义QBF知识库的QHorn近似的概念,然后给出两个具体的算法QHorn-GLB和QHorn-UB来计算QBF知识库的最大QHorn下界(GLB)和QHorn上界(UB),并且证明了这两个算法计算的结果是正确的,最后给出了利用QHorn近似进行推理的方法。实验结果表明,该方法能有效地处理QBF知识库的知识编译问题,并能在多项式时间内回答对原知识库的查询。