File(s) under permanent embargo
Reason: This item is currently closed access.
Decidable cases of first-order temporal logic with functions
journal contributionposted on 08.04.2008, 07:54 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