resolution based theorem prover for temporal logic
Your translation goes into Presburger arithmetic, which is decidable. 

You could take your translated formula, do quantifier elimination on it, and then hand it over to a proof-producing SMT solver. Since pretty much all SMT solvers are (fancy extensions of) DPLL, I would guess you can turn those proofs into resolution proofs without too much difficulty. 

I'm pretty sure that CVC4 can directly give you the resolution proofs, and would be surprised if Z3 couldn't.