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·p, 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. (shrink)

Many logics considered in finite model theory have a natural notion of an arity. The purpose of this article is to study the hierarchies which are formed by the fragments of such logics whose formulae are of bounded arity.Based on a construction of finite graphs with a certain property of homogeneity, we develop a method that allows us to prove that the arity hierarchies are strict for several logics, including fixed-point logics, transitive closure logic and its deterministic version, variants of (...) the database language Datalog, and extensions of first-order logic by implicit definitions.Furthermore, we show that all our results already hold on the class of finite graphs. (shrink)

We study a refined framework of parameterized complexity theory where the parameter dependence of fixed-parameter tractable algorithms is not arbitrary, but restricted by a function in some family . For every family of functions, this yields a notion of -fixed-parameter tractability. If is the class of all polynomially bounded functions, then -fixed-parameter tractability coincides with polynomial time decidability and if is the class of all computable functions, -fixed-parameter tractability coincides with the standard notion of fixed-parameter tractability. There are interesting choices (...) of between these two extremes, for example the class of all singly exponential functions. In this article, we study the general theory of -fixed-parameter tractability. We introduce a generic notion of reduction and two classes -W[P] and -XP, which may be viewed as analogues of NP and EXPTIME, respectively, in the world of -fixed-parameter tractability. (shrink)

In this paper we prove that thek-ary fragment of transitive closure logic is not contained in the extension of the (k−1)-ary fragment of partial fixed point logic by all (2k−1)-ary generalized quantifiers. As a consequence, the arity hierarchies of all the familiar forms of fixed point logic are strict simultaneously with respect to the arity of the induction predicates and the arity of generalized quantifiers.Although it is known that our theorem cannot be extended to the sublogic deterministic transitive closure logic, (...) we show that an extension is possible when we close this logic under congruence. (shrink)

We prove an existential version of Gaifman's locality theorem and show how it can be applied algorithmically to evaluate existential first-order sentences in finite structures.

Throughout the development of finite model theory, the fragments of first-order logic with only finitely many variables have played a central role. This survey gives an introduction to the theory of finite variable logics and reports on recent progress in the area.For each k ≥ 1 we let Lk be the fragment of first-order logic consisting of all formulas with at most k variables. The logics Lk are the simplest finite-variable logics. Later, we are going to consider infinitary variants and (...) extensions by so-called counting quantifiers.Finite variable logics have mostly been studied on finite structures. Like the whole area of finite model theory, they have interesting model theoretic, complexity theoretic, and combinatorial aspects. For finite structures, first-order logic is often too expressive, since each finite structure can be characterized up to isomorphism by a single first-order sentence, and each class of finite structures that is closed under isomorphism can be characterized by a first-order theory. The finite variable fragments seem to be promising candidates with the right balance between expressive power and weakness for a model theory of finite structures. This may have motivated Poizat [67] to collect some basic model theoretic properties of the Lk. Around the same time Immerman [45] showed that important complexity classes such as polynomial time or polynomial space can be characterized as collections of all classes of finite structures definable by uniform sequences of first-order formulas with a fixed number of variables and varying quantifier-depth. (shrink)

We discuss several possible extensions of the classical Löwenheim-Skolem Theorem to finite structures and give a counterexample refuting almost all of them.

We observe that the W*-hierarchy, a variant (introduced by Downey, Fellows, and Taylor [7]) of the better known W-hierarchy, coincides with the W-hierarchy, though not level wise, but just as a whole hierarchy. More precisely, we prove that W[t] ⊆ W*[t] ⊆ W[2t − 2] for each t ≥ 2. It was known before that W[1] = W*[1] and W[2] = W*[2]. Our second main result is a new logical characterization of the W*-hierarchy in terms of "Fagin-definable problems." As a (...) by-product, we also obtain an improvement of our earlier characterization of the hierarchy in terms of model-checking problems. Furthermore, we obtain new complete problems for the classes W[3] and W*[3]. (shrink)

Increasingly, medical educators integrate art-viewing into curricular interventions that teach clinical observation—often with local art museum educators. How can cross-disciplinary collaborators explicitly connect the skills learned in the art museum with those used at the bedside? One approach is for educators to align their pedagogical approach using similar teaching methods in the separate contexts of the galleries and the clinic. We describe two linked pedagogical exercises—Visual Thinking Strategies (VTS) in the museum galleries and observation at the bedside—from “Training the Eye: (...) Improving the Art of Physical Diagnosis,” an elective museum-based course at Harvard Medical School. It is our opinion that while strategic interactions with the visual arts can improve skills, it is essential for students to apply them in a clinical context with faculty support—requiring educators across disciplines to learn from one another. (shrink)