Automated Theorem Proving in Temporal Logic：T—Resolution
招兆铿, 戴军, 陈文丹 · 1994
This paper presentes a novel resolution method,T-resolution,based on the first order temporal logic.The primary claim of this method is its soundness and completeness.For this purpose,we construct the corresponding semantic trees and extend Herbrand's Theorem.