Decidable fragments of first-order temporal logics
type: Item
instance of: scholarly article
title: Decidable fragments of first-order temporal logics
zbMATH Open document ID: 0999.03015
DOI: 10.1016/S0168-0072(00)00018-X
author: F. Wolter
author: Ian Hodkinson
author: Michael Zakharyaschev
published in: Annals of Pure and Applied Logic
publication date: 2002-11-28T00:00:00Z
review text: First-order temporal logic extends ordinary first-order logic by the binary temporal operators \({\mathcal S}\) (since) and \({\mathcal U}\) (until). The logic is interpreted using a strict linear order \((W,<)\) and for each \(w\in W\) a first-order structure \(I(w)\) where the underlying domain of the \(I(w)\) as well as the interpretations of constants are the same for each \(w\). The linear order \(W\) models the flow of time; \(I(w)\) varying with \(w\) reflects the idea that meanings of predicates may change over time. Given \(w\in W\) and a formula \(\phi\) with parameters from \(D\), one writes \(w\models \phi\) to mean that \(\phi\) is valid ``at time'' \(w\). One has in particular \(w\models \phi{\mathcal U}\psi\) iff there is \(v>w\) such that \(v\models \phi\) and \(u\models \psi\) for each \(w<u<v\). Likewise, \(w\models \phi{\mathcal S}\psi\) iff there is \(v<w\) such that \(v\models \phi\) and \(u\models \psi\) for each \(v<u<w\). For example, \(\diamondsuit\phi := \top{\mathcal U}\phi\) expresses that \(\phi\) holds at some later time, i.e., eventually, whereas \(\square\phi:=\neg\diamondsuit\neg\phi\) expresses that \(\phi\) holds at all later times, i.e., henceforth. Unfortunately, already the monadic fragment (only unary predicate symbols) as well as the 2-variable fragments (formulas contain at most two distinct variables) are not even recursively enumerable, i.e., there does not exist a recursive axiomatisation of the formulas that are true for some interpretation. This is proved by reduction to the recurrent tiling problem for \({\mathbf N}\times {\mathbf N}\). The situation does not change if one restricts attention to interpretation in finite domains (but over infinite time, e.g., \(W=({\mathbf N},<))\). Notice that the corresponding fragments of pure first-order logic are decidable. The contribution of the paper is that decidability of satisfiability can be regained if a) one restricts the purely first-order part to a decidable fragment and …
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 68P15
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68T30
Mathematics Subject Classification ID: 03D35
zbMATH DE Number: 1546600
zbMATH Keywords: first-order temporal logic
zbMATH Keywords: temporal databases
zbMATH Keywords: classical decision problem
zbMATH Keywords: decidable fragments
zbMATH Keywords: decidability
zbMATH Keywords: undecidability
MaRDI profile type: Publication
cites work: Modal languages and bounded fragments of predicate logic
cites work: A survey of temporal extensions of description logics
cites work: A multi-dimensional terminological knowledge representation language
cites work: Q5691140
cites work: Q5525343
cites work: The decision problem for linear temporal logic
cites work: Q4518442
cites work: On the feasibility of checking temporal integrity constraints
cites work: Q4845472
cites work: Q3835817
cites work: Temporal logic. Vol. 2. Mathematical foundations and computational aspects
cites work: Products of modal logics, part 1
cites work: Q4342097
cites work: On the Restraining Power of Guards
cites work: Elementary properties of ordered abelian groups
cites work: Expanded theory of ordered Abelian groups
cites work: Q4003410
cites work: To the memory of Arthur Prior Formal properties of ‘now’
cites work: On the elementary theory of linear order
cites work: Decidability and incompleteness results for first-order temporal logics of linear time
cites work: On languages with two variables
cites work: Q3746875
cites work: Decidability of Second-Order Theories and Automata on Infinite Trees
cites work: Axiomatising first-order temporal logic: Until and since over linear time
cites work: Q3949052
cites work: Temporal aspects of logical procedure definition
cites work: Q4023900
cites work: Concerning the semantic consequence relation in first-order temporal logic
cites work: Incompleteness of first-order temporal logic with until
cites work: Temporalizing description logics
cites work: Decidable fragments of first-order modal logics
full work available at URL: s0168-0072(00)00018-x
OpenAlex ID: W2045554431
description: scientific article; zbMATH DE number 1546600