期刊文献+

命题时态逻辑矢列式演算系统 被引量:1

原文传递
导出
摘要 研究Manna和Pnueli在并发程序验证方面提出的一种时态逻辑,其时间结构与自然数结构同构,时态算子选择为□,◇,○,U。本文作者认真分析了国际上时态逻辑定理证明主要方法,针对存在的不足之处,建立了命题时态逻辑矢列式演算系统,并证明了该系统的可靠性和完全性。
出处 《中国科学(A辑)》 CSCD 1994年第10期1092-1098,共7页 Science in China(Series A)
基金 国家"八六三"高科技软件生产自动化课题 国家自然科学基金资助项目
  • 相关文献

参考文献3

  • 1贲可荣,陈火旺.PTL证明器的实现技术[J].国防科技大学学报,1994,16(1):53-59. 被引量:1
  • 2Laurent Catach. TABLEAUX: A general theorem prover for modal logics[J] 1991,Journal of Automated Reasoning(4):489~510
  • 3David A. Plaisted. A decision procedure for combinations of propositional temporal logic and other specialized theories[J] 1986,Journal of Automated Reasoning(2):171~190

二级参考文献3

  • 1赉可荣,软件学报,1994年,5卷,5期
  • 2赉可荣,计算机科学,1993年,20卷,4期
  • 3赉可荣,中国科学

同被引文献1

引证文献1

二级引证文献2

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部