Temporalising tableaux
type: Item
instance of: scholarly article
title: Temporalising tableaux
zbMATH Open document ID: 1050.03015
author: Roman Kontchakov
author: Carsten Lutz
author: F. Wolter
author: Michael Zakharyaschev
published in: Studia Logica
publication date: 2004-08-06T00:00:00Z
review text: The monodic fragments of first-order temporal logic (FOTL) are obtained by restricting the application of temporal operators to formulas with at most one free variable. This paper is concerned with constructing tableau algorithms for monodic fragments based on decidable fragments of FOTL like the two-variable fragment or the guarded fragment. A general framework is presented that shows how existing decision procedures for first-order fragments can be used for constructing a tableau algorithm for the corresponding monodic fragment of FOTL. Some example instantiations of the framework are presented.
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 2081423
zbMATH Keywords: first-order temporal logic
zbMATH Keywords: monodic fragment
zbMATH Keywords: tableau algorithm
reviewed by: Giacomo Bonanno
MaRDI profile type: Publication
full work available at URL: b:stud.0000027468.28935.6d
OpenAlex ID: W4244421355
DOI: 10.1023/B:STUD.0000027468.28935.6D
Recommended article: Q4251979
Recommended article: Temporal dynamics in information tables
Recommended article: Q3710510
Recommended article: Q4539602
Recommended article: Q4373589
Recommended article: Tableaux for logics of time and knowledge with interactions relating to synchrony
Recommended article: Temporal structures
Recommended article: Temporal Structures
Recommended article: A tableau for general linear temporal logic
Recommended article: A tableau construction for finite linear-time temporal logic
description: scientific article; zbMATH DE number 2081423