基于时序逻辑的Resolution自动定理证明方法

　　章岚，2011年毕业于英国利物浦大学，并获得博士学位（专业方向：计算机科学）。　主要研究方向为人工智能，计算机逻辑，形式化验证（Formal Verification，Theoremproving）。　主讲课程为《电子商务系统分析》、《数据库应用》、《专业外语》等。

时序逻辑是人工智能和计算机科学领域中的重要建模工具。随着时序逻辑的广泛使用，应用时序逻辑来对复杂系统进行推理和验证的算法也应运而生。其中最成功的方法之一就是Resolution算法，这也是本书的主题。 1965年美国数理逻辑专家鲁滨逊（J. A. Robinson）提出了一条Resolution推理规则，这标志着Resolution算法的起点。因其简洁性（整个推理过程中只使用一条推理规则）和便于机械操作的特点，Resolution算法得到了各国学者的重视，并且在各国学者的推动下发展得非常迅速。经过几十年的发展和持续的改进，到目前为止，Resolution算法在经典逻辑中已经趋于成熟。 本书主要聚焦Resolution算法在时序逻辑领域的研究，详细介绍了把Resolution算法从表达能力较弱的时序逻辑逐渐向表达能力较强的时序逻辑进行拓展和优化的研究成果。主要涉及以下几种时序逻辑： （1）线性时序逻辑（Propositional Linear-Time Temporal Logic） （2）计算树逻辑（Computation Tree Logic）和其扩展（Extended Computation Tree Logic） （3）交互时序逻辑（Alternating-Time Temporal Logic）