Axiomatizing the monodic fragment of first-order temporal logic
type: Item
instance of: scholarly article
title: Axiomatizing the monodic fragment of first-order temporal logic
zbMATH Open document ID: 1031.03023
DOI: 10.1016/S0168-0072(01)00124-5
author: F. Wolter
author: Michael Zakharyaschev
published in: Annals of Pure and Applied Logic
publication date: 2002-12-02T00:00:00Z
review text: It is shown that the fragment of the first-order temporal logic over the natural numbers that has no functional symbols, no equality and contains only monodic formulas, i.e., all those where each temporal subformula has at most one free variable, can be given a Hilbert-style axiomatization. Moreover, adding equality yields a theory which is not recursively enumerable. Finally the paper shows that the monodic fluted fragment and the monodic loosely guarded fragment are decidable.
reviewed by: Petr Jančar
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 1838869
zbMATH Keywords: first-order temporal logic
zbMATH Keywords: axiomatizability
zbMATH Keywords: decidability
MaRDI profile type: Publication
cites work: Q5691140
cites work: On the feasibility of checking temporal integrity constraints
cites work: Q4400800
cites work: Q3835817
cites work: Q3773852
cites work: Q4263155
cites work: Decidable fragments of first-order temporal logics
cites work: Decidability of fluted logic with identity
cites work: Fluted formulas and the limits of decidability
description: scientific article; zbMATH DE number 1838869