一句话：提出模分解定理，将图类可定义规范化归约到素图，并证明带计数的固定点逻辑在置换图上捕获多项式时间。
描述复杂性理论长期关注是否存在捕获多项式时间的逻辑。Grohe 曾证明带计数的固定点逻辑在排除子式图上捕获 PTIME；本文转向排除诱导子图的图类，利用 Gallai 的模分解。作者提出模分解定理，把图类 C 的可定义规范化归约到其素图（带线性序集合上的二元关系着色）的可定义规范化。应用该定理，证明带计数的固定点逻辑在置换图上捕获多项式时间。证明中还表明图的模分解可在带计数的对称传递闭包逻辑中定义，由此模分解树可在对数空间计算，并推出余图识别与规范化也可在对数空间完成。
The question of whether there is a logic that captures polynomial time is one of the main open problems in descriptive complexity theory and database theory. In 2010 Grohe showed that fixed point logic with counting captures polynomial time on all classes of graphs with excluded minors. We now consider classes of graphs with excluded induced subgraphs. For such graph classes, an effective graph decomposition, called modular decomposition, was introduced by Gallai in 1976. The graphs that are non-decomposable with respect to modular decomposition are called prime. We present a tool, the Modular Decomposition Theorem, that reduces (definable) canonization of a graph class C to (definable) canonization of the class of prime graphs of C that are colored with binary relations on a linearly ordered set. By an application of the Modular Decomposition Theorem, we show that fixed point logic with counting captures polynomial time on the class of permutation graphs. Within the proof of the Modular Decomposition Theorem, we show that the modular decomposition of a graph is definable in symmetric transitive closure logic with counting. We obtain that the modular decomposition tree is computable in logarithmic space. It follows that cograph recognition and cograph canonization is computable in logarithmic space.Comment: 38 pages, 10 Figures. A preliminary version of this article appeared in the Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '17)