A Natural Deduction System of Temporal Logic

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