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

1星价 ¥27.0 (4.9折)

2星价￥27.0 定价￥55.0

作者：章岚

出版社：首都经济贸易大学出版社

本类榜单：计算机/网络

分类：计算机/网络 > 程序设计 > 其他

温馨提示：5折以下图书主要为出版社尾货，大部分为全新（有塑封/无塑封），个别图书品相8-9成新、切口有划线标记、光盘等附件不全详细品相说明>>

暂无评论

图文详情

ISBN：9787563832668
装帧：一般胶版纸
册数：暂无
重量：暂无
开本：16开
页数：240
出版时间：2021-09-01
条形码：9787563832668 ; 978-7-5638-3266-8

内容简介

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

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

展开全部