Sciweavers

Share
SLOGICA
2008

Decidable Cases of First-order Temporal Logic with Functions

9 years 4 months ago
Decidable Cases of First-order Temporal Logic with Functions
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.
Walter Hussak
Added 28 Jan 2011
Updated 28 Jan 2011
Type Journal
Year 2008
Where SLOGICA
Authors Walter Hussak
Comments (0)
books