%0 Journal Article
%T A NEW METHOD FOR THEOREM PROVING OF PTL<br>命题时态逻辑定理证明新方法
%A Ben Kerong
%A Chen Huowang
%A <br>贲可荣
%A 陈火旺
%J 软件学报
%D 1994
%I 
%X 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.
%K Temporal logic
%K theorem proving
%K automated reasoning<br>时态逻辑，定理证明，自动推理
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=69703006FA0C9ECDD3A4C0D992C50D1D&yid=3EBE383EEA0A6494&vid=94C357A881DFC066&iid=DF92D298D3FF1E6E&sid=659D3B06EBF534A7&eid=D3E34374A0D77D7F&journal_id=1000-9825&journal_name=软件学报&referenced_num=1&reference_num=11