Tractability results for the model checking problem of logics yield powerful algorithmic meta theorems of the form: Every computational problem expressible in a logic $L$ can be solved efficiently on every class $\mathscr{C}$ of structures satisfying certain conditions. The most prominent logics studied in the field are (counting) monadic second-order logic (C)MSO, and first-order logic FO and its extensions. The complexity of CMSO model checking in general and of FO model checking on monotone graph classes is very well understood. In recent years there has been a rapid and exciting development of new algorithmic meta theorems. On the one hand there has been major progress for FO model checking on hereditary graph classes. This progress was driven by the development of a combinatorial structure theory for the logically defined monadically stable and monadically dependent graph classes, as well as by the advent of the new width measure twinwidth. On the other hand, new algorithmic meta theorems for new logics with expressive power between FO and CMSO offer a new unifying view on methods like the irrelevant vertex technique and recursive understanding. In this paper we overview the recent advances in algorithmic meta theorems and provide rough sketches for the methods to prove them.

翻译：逻辑模型检测问题的可处理性结果产生了强大的算法元定理，其形式为：在满足特定条件的每个结构类 $\mathscr{C}$ 上，逻辑 $L$ 可表达的每个计算问题都能被高效求解。该领域研究的最主要逻辑包括（计数）单子二阶逻辑 (C)MSO、一阶逻辑 FO 及其扩展。CMSO 模型检测的复杂度，以及 FO 在单调图类上的模型检测复杂度，已得到非常深入的理解。近年来，新的算法元定理取得了快速而令人振奋的发展。一方面，FO 在遗传图类上的模型检测取得了重大进展。这一进展由逻辑定义的单调稳定和单调依赖图类的组合结构理论的发展，以及新宽度度量 twinwidth 的出现所推动。另一方面，表达能力介于 FO 与 CMSO 之间的新逻辑所对应的新算法元定理，为诸如无关顶点技术和递归理解等方法提供了新的统一视角。本文概述了算法元定理的最新进展，并提供了证明这些定理所用方法的概要草图。