The paper continues our studies of natural deduction calculus for the propositional linear-time temporal logic PLTL. We present a new formulation of natural deduction calculus for PLTL. The system is shown to be sound and complete. This new formulation is simpler than the previous one, and this fact is believed to be crucial for possible appli cations of our technique as an automatic reasoning tool in a deliberative decision making framework across various AI applications.
['Alexander Bolotov', 'Oleg Grigoriev', 'Vasilyi Shangin']
A Simpler Formulation of Natural Deduction Calculus for Linear-Time Temporal Logic