Sciweavers

Share
LICS
2006
IEEE

The Boundedness Problem for Monadic Universal First-Order Logic

10 years 5 months ago
The Boundedness Problem for Monadic Universal First-Order Logic
We consider the monadic boundedness problem for least fixed points over FO formulae as a decision problem: Given a formula ϕ(X, x), positive in X, decide whether there is a uniform finite bound on the least fixed point recursion based on ϕ. Few fragments of FO are known to have a decidable boundedness problem; boundedness is known to be undecidable for many fragments. We here show that monadic boundedness is decidable for purely universal FO formulae without equality in which each non-recursive predicate occurs in just one polarity (e.g., only negatively). The restrictions are shown to be essential: waving either the polarity constraint or allowing positive occurrences of equality, the monadic boundedness problem for universal formulae becomes undecidable. The main result is based on a model theoretic analysis involving ideas from modal and guarded logics and a reduction to the monadic second-order theory of trees.
Martin Otto
Added 12 Jun 2010
Updated 12 Jun 2010
Type Conference
Year 2006
Where LICS
Authors Martin Otto
Comments (0)
books