File(s) under permanent embargo
Reason: This item is currently closed access.
Decidable cases of first-order temporal logic with functions
journal contributionposted on 2008-04-08, 07:54 authored by Walter HussakWalter Hussak
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.
- Computer Science
CitationHUSSAK, W., 2008. Decidable cases of first-order temporal logic with functions. Studia Logica, 88 (2), pp. 247-261
NotesThis article is Restricted Access. The definitive version is available at: http://www.springerlink.com/content/0039-3215