一句话：证明 CFI 图在 Z_{2^i} 上的同构问题不可由秩逻辑定义但可由 CPT 定义，从而分离秩逻辑与多项式时间。
在寻找能刻画多项式时间的逻辑时，秩逻辑与无选择多项式时间（CPT）是两个重要候选。本文研究秩逻辑的表达能力，聚焦 CFI 图在环 Z_{2^i} 上的同构问题。作者证明该同构问题即使在底图全序化后也无法在秩逻辑中定义，而 CPT 可以定义它。由此将秩逻辑与 CPT 分离，并进一步表明秩逻辑不能刻画多项式时间，否定其作为 PTIME 逻辑候选的地位。
In the search for a logic capturing polynomial time the most promising candidates are Choiceless Polynomial Time (CPT) and rank logic. Rank logic extends fixed-point logic with counting by a rank operator over prime fields. We show that the isomorphism problem for CFI graphs over ${{\mathbb{Z}}_{{2^i}}}$ cannot be defined in rank logic, even if the base graph is totally ordered. However, CPT can define this isomorphism problem. We thereby separate rank logic from CPT and in particular from polynomial time.
DOI 原文 ·
@inproceedings{paperbot6203,
title = {Separating Rank Logic from Polynomial Time},
author = {Moritz Lichter},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470598}
}