2.1 命题知识表示与推理
知识表示与推理是人工智能中的一个重要领域。早在 1958 年，麦卡锡考虑的人工智能系统建议采纳者（Advice Taker [1]，其可被视为第一个完整的人工智能系统[2]）已主张采用知识求解问题。目前，知识表示与推理方法的应用涵盖了人工智能领域的多个应用分支，包括形式化验证、问答系统、语义网、自动规划、感知机器人和多智能体系统在内的多个领域[3]。
逻辑是一种使用时间最长，且应用最为广泛的知识表示方法，几 乎所有其它知识表示方法都能够使用某种逻辑进行等价表示。早在计 算机时代到来之前，数理逻辑学家就已开始使用经典逻辑形式化表示 陈述性的知识，主要为了对数学进行形式化，以自动进行定理证明。尽管经典逻辑在某些情况下不能表达人工智能中各式各样的非数学 形式的知识，但毫无疑问其仍然在知识表示领域占有举足轻重的地位，其中一阶逻辑由于其极强的表达能力、易理解的基于模型论的语义以 及较好的推理能力而应用最为广泛。研究人员为一阶逻辑提出了多种 的推理方法，例如 Tableau 方法[4]、DP 方法[5]、归结方法[6]等，开发 了包括Otter[7]、3TAP[8]、Isabelle[9]等在内的多个推理机。
一阶逻辑最大的问题在于其推理代价过于昂贵，命题逻辑是一阶逻辑的子集，近二十多年来随着命题可满足性（satisfiability，SAT）问题求解器效率的快速提高，其在人工智能中发挥着越来越重要的作用[10]。从本质上讲，SAT 求解器提供的是一个通用的命题推理平台，但是其可应用于推理之外的多个组合优化领域。例如，自动规划问题是 PSPACE 完全的，当规划解的长度被限制为多项式时，该问题为 NP 完全问题，可编码为 SAT 问题，著名的 SatPlan 规划器[11]在该思想的基础上实现，其在国际规划竞赛中多次夺得第一名。另外，在有界模型检测（bounded model checking）[12]和回答集编程[13]等领域，SAT
求解器都有重要应用。实际上，很多组合优化问题，通过编码为 SAT问题后再调用 SAT 求解器的求解效率甚至高于直接求解原问题的效率[3]。