A NEW METHOD FOR THEOREM PROVING OF PTL
命题时态逻辑定理证明新方法

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.