命题时态逻辑矢列式演算系统

研究Manna和Pnueli在并发程序验证方面提出的一种时态逻辑,其时间结构与自然数结构同构,时态算子选择为□,◇,○,U。本文作者认真分析了国际上时态逻辑定理证明主要方法,针对存在的不足之处,建立了命题时态逻辑矢列式演算系统,并证明了该系统的可靠性和完全性。