A Natural Deduction System of Temporal Logic

This paper will present a natural deduction system of temporal logic,which includes two collections ofinference rules called “horizontal inference rules” and “vertical inference rules” respectively.It is alsoproved that the system is both sound and complete under an appropriate interpretation.Very natural andgenerally short,each proof in the system can be represented by a matrix whose entries serve to record theinference process.