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

图书标准信息

• 作者 章岚
• 出版社 首都经济贸易大学出版社
• 出版时间 2021-09
• 版次 1
• ISBN 9787563832668
• 定价 55.00元
• 装帧 其他
• 开本 16开
• 纸张 胶版纸
• 页数 240页
• 字数 253.000千字

【内容简介】

时序逻辑是人工智能和计算机科学领域中的重要建模工具。随着时序逻辑的广泛使用，应用时序逻辑来对复杂系统进行推理和验证的算法也应运而生。其中成功的方法之一就是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）

【作者简介】

 章岚，2011年毕业于英国利物浦大学，并获得博士学位（专业方向：计算机科学）。

　　    主要研究方向为人工智能，计算机逻辑，形式化验证（Formal Verification,Theoremproving）。

　　    主讲课程为《电子商务系统分析》、《数据库应用》、《专业外语》等。

【目录】

Preface

Acknowledgements

1  Introduction

1.1  Formal methods for system designs

1.1.1  Formal specification

1.1.2  Formal verification

1.2  Novel contributions

2  Preliminaries to resolution for branching-time temporal logic

2.1  Propositional logic

2.1.1  Syntax and semantics of propositional logic

2.1.2  Resolution for propositional logic

2.2  Propositional linear-time temporal logic

2.2.1  Syntax and semantics of PLTL

2.2.2  Resolution for PLTL

3  A refined resolution calculus for CTL

3.1  Introduction

3.2  Syntax and semantics of CTL

3.3  Normal form

3.3.1  Syntax and semantics of SNFgTL

3.3.2  Transformation

3.4  The clausal resolution calculus RSECTL

3.4.1  Step resolution

3.4.2  Eventuality resolution

3.4.3  Loop search

3.4.4  A decision procedure

3.5  Correctness of the calculus RSECTL

3.5.1  Correctness of the transformation to SNFgTL

3.5.2  Soundness and completeness

3.5.3  Termination

3.6  Complexity

3.7  Related work

3.7.1  Comparison between RSECTL and the previous resolution calculus

3.7.2  Other approaches for the satisfiability problem of CTL

3.8  Conclusions

4  CTL-RP: A resolution theorem prover for CTL

4.1  Introduction

4.2  Implementation of the calculus RSL

4.2.1  Preliminaries of first-order ordered resolution with selection

4.2.2  Representing SNFgCTL clauses as first-order clauses

4.2.3  Implementing step resolution

4.2.4  Implementing eventuality resolution

4.2.5  The main procedure of our implementation

4.2.6  CTL-RP

4.3  Related theorem provers

4.3.1  OTRES and TRP++

4.3.2  Tableau Workbench

4.4  Performance of CTL-RP

4.4.1  CTL-RP vs. TWB

4.4.2  CTL-RP 00.14 vs. 00.09

4.5  Conclusions

5  Resolution for ECTL

5.1  Introduction

5.2  Syntax and semantics of ECTL

5.3  Normal form

5.4  The clausal resolution calculus, RSECTL

5.5  Properties of RSECTL

5.6  Conclusions and future work

6  Resolution for the Next-time fragment of ATL

6.1  Introduction

6.2  Syntax and semantics of XATL

6.2.1  Syntax of XATL

6.2.2  Semantics of XATL

6.3  Normal form

6.3.1  Normal form for XATL SNFXATL

6.3.2  Semantics of SNFxATL

6.3.3  Transformation

6.4  The clausal resolution calculus RXATL

6.5  Correctness of the calculus RXATL

6.5.1  Correctness of the transformation

6.5.2  Soundness and completeness

6.6  Conclusions

7  Conclusions and future work

7.1  Conclusions

7.2  Future work

7.2.1  Further research on XATL resolution

7.2.2  Extension to other modal logics

Appendix

Bibliography

内容摘要

时序逻辑是人工智能和计算机科学领域中的重要建模工具。随着时序逻辑的广泛使用，应用时序逻辑来对复杂系统进行推理和验证的算法也应运而生。其中成功的方法之一就是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）

 

主编推荐

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