一句话:提出带群阶算子的不动点逻辑 FP+ord,可多项式时间模型检测,并刻画更广的多项式时间可计算查询。
本文针对不动点逻辑 FP 无法刻画多项式时间可计算查询 P 的问题,引入群阶算子 ord,用于计算由可定义置换集合生成的群的阶。该算子是秩算子 rk 的推广,由此得到新逻辑 FP + ord,并把它作为 P 的新候选逻辑。作者证明 FP + ord 的模型检测仍是多项式时间可计算的;进一步,Lichter 最近工作中用于区分 FP + rk 与 P 的查询可在 FP + ord 中定义。证明关键在于在 FP + ord 内表达图规范化群论方法的一个片段,并据此规范化具有交换颜色的结构,而该结构类包含 Lichter 的反例。
We introduce an extension of fixed-point logic (FP) with a group-order operator (ord), that computes the size of a group generated by a definable set of permutations. This operation is a generalization of the rank operator (rk). We show that FP + ord constitutes a new candidate logic for the class of polynomial-time computable queries (P). As was the case for FP + rk, the model-checking of FP + ord formulae is polynomial-time computable. Moreover, the query separating FP + rk from P exhibited by Lichter in his recent breakthrough is definable in FP + ord. Precisely, we show that FP + 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 FP + ord.