A labelled natural deduction system for linear temporal logic
type: Item
instance of: scholarly article
title: A labelled natural deduction system for linear temporal logic
zbMATH Open document ID: 1038.03016
author: Andrzej Indrzejczak
published in: Studia Logica
publication date: 2004-01-14T00:00:00Z
review text: 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.
reviewed by: Bernhard Heinemann
Mathematics Subject Classification ID: 03B44
zbMATH DE Number: 2027185
zbMATH Keywords: natural deduction
zbMATH Keywords: labelling
zbMATH Keywords: linear temporal logic
zbMATH Keywords: \textbf{Kt4.3}
zbMATH Keywords: linear time
describes a project that uses: KtSeqC
MaRDI profile type: Publication
full work available at URL: b:stud.0000009565.98020.9b
OpenAlex ID: W2075766564
DOI: 10.1023/B:STUD.0000009565.98020.9B
description: scientific article; zbMATH DE number 2027185