@article{FRICK20043,
    Abstract = {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)·p(n), for any elementary function f and any polynomial p. Here k denotes the size of the input sentence and n the size of the input word. We establish a number of similar lower bounds for the model-checking problem for first-order logic, for example, on the class of all trees.},
    Author = {Frick, Markus and Grohe, Martin},
    File = {The complexity of first-order and monadic second-order logic revisited - FrickGrohe - a - a - a - n.pdf},
    ISSN = {0168-0072},
    Journal = {Annals of Pure and Applied Logic},
    Note = {Papers presented at the 2002 IEEE Symposium on Logic in Computer Science (LICS)},
    Number = {1},
    Pages = {3 - 31},
    Title = {The complexity of first-order and monadic second-order logic revisited},
    URL = {http://www.sciencedirect.com/science/article/pii/S0168007204000612},
    Volume = {130},
    Year = {2004},
    bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0168007204000612},
    bdsk-url-2 = {https://doi.org/10.1016/j.apal.2004.01.007},
    date-added = {2020-01-23 10:25:18 +0100},
    date-modified = {2020-01-23 10:25:18 +0100},
    doi = {10.1016/j.apal.2004.01.007}
}

@article{FRICK20043, Abstract = {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)·p(n), for any elementary function f and any polynomial p. Here k denotes the size of the input sentence and n the size of the input word. We establish a number of similar lower bounds for the model-checking problem for first-order logic, for example, on the class of all trees.}, Author = {Frick, Markus and Grohe, Martin}, File = {The complexity of first-order and monadic second-order logic revisited - FrickGrohe - a - a - a - n.pdf}, ISSN = {0168-0072}, Journal = {Annals of Pure and Applied Logic}, Note = {Papers presented at the 2002 IEEE Symposium on Logic in Computer Science (LICS)}, Number = {1}, Pages = {3 - 31}, Title = {The complexity of first-order and monadic second-order logic revisited}, URL = {http://www.sciencedirect.com/science/article/pii/S0168007204000612}, Volume = {130}, Year = {2004}, bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0168007204000612}, bdsk-url-2 = {https://doi.org/10.1016/j.apal.2004.01.007}, date-added = {2020-01-23 10:25:18 +0100}, date-modified = {2020-01-23 10:25:18 +0100}, doi = {10.1016/j.apal.2004.01.007} }