Decidable Cases of First-order Temporal Logic with Functions

Studia Logica 88 (2):247-261 (2008)
  Copy   BIBTEX

Abstract

We consider the decision problem for cases of first-order temporal logic with function symbols and without equality. The monadic monodic fragment with flexible functions can be decided with EXPSPACE-complete complexity. A single rigid function is sufficient to make the logic not recursively enumerable. However, the monadic monodic fragment with rigid functions, where no two distinct terms have variables bound by the same quantifier, is decidable and EXPSPACE-complete.

Categories

Keywords

Reprint years

DOI

10.1007/s11225-008-9104-y

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,323

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

An Event-Based Fragment of First-Order Logic over Intervals.Savas Konur - 2011 - Journal of Logic, Language and Information 20 (1):49-68.
Decidable fragments of first-order temporal logics.Ian Hodkinson, Frank Wolter & Michael Zakharyaschev - 2000 - Annals of Pure and Applied Logic 106 (1-3):85-134.
An Undecidable Linear Order That Is $n$-Decidable for All $n$.John Chisholm & Michael Moses - 1998 - Notre Dame Journal of Formal Logic 39 (4):519-526.
Decidable properties for monadic abstract state machines.Daniele Beauquier - 2006 - Annals of Pure and Applied Logic 141 (3):308-319.
Pure Second-Order Logic with Second-Order Identity.Alexander Paseau - 2010 - Notre Dame Journal of Formal Logic 51 (3):351-360.
Logical Consecutions in Discrete Linear Temporal Logic.V. V. Rybakov - 2005 - Journal of Symbolic Logic 70 (4):1137 - 1149.
On countable chains having decidable monadic theory.Alexis Bés & Alexander Rabinovich - 2012 - Journal of Symbolic Logic 77 (2):593-608.
Adding a temporal dimension to a logic system.Marcelo Finger & Dov M. Gabbay - 1992 - Journal of Logic, Language and Information 1 (3):203-233.
On a decidable generalized quantifier logic corresponding to a decidable fragment of first-order logic.Natasha Alechina - 1995 - Journal of Logic, Language and Information 4 (3):177-189.
Expressive completeness of temporal logic of trees.Bernd-Holger Schlingloff - 1992 - Journal of Applied Non-Classical Logics 2 (2):157-180.
Satisfiability of formulae with one ∀ is decidable in exponential time.Erich Grädel - 1990 - Archive for Mathematical Logic 29 (4):265-276.
Elementary equivalence of some rings of definable functions.Vincent Astier - 2008 - Archive for Mathematical Logic 47 (4):327-340.
Periodicity Based Decidable Classes in a First Order Timed Logic.Danièle Beauquier & Anatol Slissenko - 2006 - Annals of Pure and Applied Logic 139 (1):43-73.
A Decidable Temporal Logic of Parallelism.Mark Reynolds - 1997 - Notre Dame Journal of Formal Logic 38 (3):419-436.
Decidability Results for Metric and Layered Temporal Logics.Angelo Montanari & Alberto Policriti - 1996 - Notre Dame Journal of Formal Logic 37 (2):260-282.

Analytics

Added to PP
2009-01-28

Downloads
37 (#434,087)

6 months
2 (#1,206,262)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Decidable fragments of first-order temporal logics.Ian Hodkinson, Frank Wolter & Michael Zakharyaschev - 2000 - Annals of Pure and Applied Logic 106 (1-3):85-134.

Add more references