Based on the theory of [10], the propositional temporal logic (PTL) prover has been implemented in Turbo-Prolog and runs on 386 microcomputers. The PTL prover has some original features in dealing with the power of next, induction, resolution, ◇(xΛy), until，The prover's many full-screen facilities make it easy to use. The prover appears to be of reasonable efficiency for most current examples.