| 摘要: |
| 本文通过对近１０年命题时态逻辑定理证明方法的研究，提出了一种新的证明方法，前人的工作基于对公式的现时部分和后时部分的分解，本文的工作是基于语义反驳树构造。这种新方法为计算机自动证明命题时态逻辑定理，提供了比较好的理论框架．最后还证明了该方法的可靠性和完全性． |
| 关键词: 时态逻辑，定理证明，自动推理 |
| DOI： |
| 分类号: |
| 基金项目:软件生产自动化课题 |
|
| A NEW METHOD FOR THEOREM PROVING OF PTL |
|
Ben Kerong,Chen Huowang
|
| Abstract: |
| n this paper, a new method for theorem proving of PTL (propositional temporal logic) based on constructing semantic refutation tree is presented. This method,which is different from the other existed methods all based on decomposing a temporal formula into now-part and next-part, provides a well theory framework for automatic theorem proving of PTL. The soundness and completeness of this method are also proved. |
| Key words: Temporal logic theorem proving automated reasoning. |
