本文主要针对基于自动推理技术的规划方法予以研究，分别考虑经典规划问题基于命题逻辑的规划方法和规划问题基于模态逻辑的规划方法，主要包括如下工作: 1)综述基于自动推理技术的规划方法的研究现状。 2)提出基于Graphplan的编码和基于状态的编码中重叠公理的判定策略和冗余公理的删除策略;在基于Graphplan的编码方式的基础上，通过压缩动作互斥公理和添加框架公理设计并实现两种新的编码方式:基于PMA的编码方式和基于FA的编码方式。 3)在基于动作的编码方式的基础上，提出一种新的利用约简动作变元得到的、仅依赖于表示状态的命题变元的编码方式:基于命题的编码方式。