标题： 群论逻辑 显示英文标题

标题： Group Order Logic

摘要： 我们引入了固定点逻辑（$\mathsf{FP}$）的一种扩展，其中包含一个群阶运算符（$\mathsf{ord}$），该运算符计算由可定义的置换集生成的群的大小。 此操作是秩运算符（$\mathsf{rk}$）的推广。 我们证明了$\mathsf{FP} + \mathsf{ord}$构成多项式时间内可计算查询（$\mathsf{P}$）类的一个新候选逻辑。 正如$\mathsf{FP} + \mathsf{rk}$的情况一样，对$\mathsf{FP} + \mathsf{ord}$公式的模型检测是可以在多项式时间内计算的。 此外，Lichter在他近期的突破中所展示的用于区分$\mathsf{FP} + \mathsf{rk}$和$\mathsf{P}$的查询可以在$\mathsf{FP} + \mathsf{ord}$中定义。具体来说，我们证明了$\mathsf{FP} + \mathsf{ord}$可以规范化具有交换颜色的结构，这一类结构包含了Lichter的反例。此证明涉及将图规范化的方法中的群论部分表达为逻辑$\mathsf{FP}+ \mathsf{ord}$的片段。 显示英文摘要

摘要： We introduce an extension of fixed-point logic ($\mathsf{FP}$) with a group-order operator ($\mathsf{ord}$), that computes the size of a group generated by a definable set of permutations. This operation is a generalization of the rank operator ($\mathsf{rk}$). We show that $\mathsf{FP} + \mathsf{ord}$ constitutes a new candidate logic for the class of polynomial-time computable queries ($\mathsf{P}$). As was the case for $\mathsf{FP} + \mathsf{rk}$, the model-checking of $\mathsf{FP} + \mathsf{ord}$ formulae is polynomial-time computable. Moreover, the query separating $\mathsf{FP} + \mathsf{rk}$ from $\mathsf{P}$ exhibited by Lichter in his recent breakthrough is definable in $\mathsf{FP} + \mathsf{ord}$. Precisely, we show that $\mathsf{FP} + \mathsf{ord}$ canonizes structures with Abelian colors, a class of structures which contains Lichter's counter-example. This proof involves expressing a fragment of the group-theoretic approach to graph canonization in the logic $\mathsf{FP}+ \mathsf{ord}$.