Automating natural deduction for temporal logic

We present our recent work on the construction of natural deduction calculi for temporal logic. We analyse propositional linear-time temporal logic (PLTL) and Computation Tree Logic (CTL) and corresponding proof searching algorithms. The automation of the natural deduction calculi for these temporal logics opens the new prospect to apply our techniques as an automatic reasoning tool in the areas, where the linear-time or branching-time setting is required