Guarded quantification in least fixed point logic (Q1424969)

The author develops a variant of least fixed point logic based on first-order logic with a relaxed version of guarded quantification. He develops a game-theoretic semantics of this logic, and finds that under reasonable conditions, guarding quantification does not reduce the expressibility of least fixed point logic. He also finds that the guarded version of a least fixed point algorithm may have a greater time complexity than the unguarded version, by a linear factor.