On the Complexity of the Natural Deduction Proof Search Algorithm

We present our first account of the complexity of natural deduction proof search algorithms. Though we target the complexity for natural deduction for temporal logic, here we only tackle classical case, comparing the classical part of the proof search for temporal logic with the classical analytical tableau