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.