A labelled natural deduction system for linear temporal logic (Q1419387)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A labelled natural deduction system for linear temporal logic |
scientific article |
Statements
A labelled natural deduction system for linear temporal logic (English)
0 references
14 January 2004
0 references
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.
0 references
natural deduction
0 references
labelling
0 references
linear temporal logic
0 references
\textbf{Kt4.3}
0 references
linear time
0 references
