Natural deduction system for linear time temporal logic

We present a sound and complete Quine-style natural abstract deduction system for propositional linear-time temporal logic based on similar systems for the propositional classical logic. The presented system can serve as a basis for the construction of provers, which are of interest in the context of research in Articial Intelligence