The complexity of first-order and monadic second-order logic revisited

The model-checking problem for a logic L on a class C of structures asks whether a given L-sentence holds in a given structure in C. In this paper, we give super-exponential lower bounds for fixed-parameter tractable model-checking problems for first-order and monadic second-order logic. We show that unless PTIME = NP, the model-checking problem for monadic second-order logic on finite words is not solvable in time f(k)

• Type: Journal
• Year: 2004
• Where: APAL
• Authors: Markus Frick, Martin Grohe
• Keywords: APAL 2004, Lower Bounds, Model-checking Problem, Monadic Second-order Logic