A labelled natural deduction system for linear temporal logic
In this paper, a labelled natural deduction system called LND-\textbf{Kt4.3} is studied. The soundness and completeness of LND-\textbf{Kt4.3} with respect to the well-known class of all tense logic models based on a linear flow of time are proved. The possible applications to automated reasoning are discussed. A considerable part of the paper is devoted to commenting on the properties of the system (e.g., analyticity) and comparing it with related work, in particular various (natural deduction and tableau) calculi.
scientific article; zbMATH DE number 2027185