论文标题
在定点逻辑中见证了对称的选择和解释
Witnessed Symmetric Choice and Interpretations in Fixed-Point Logic with Counting
论文作者
论文摘要
寻求Ptime逻辑的核心是做出任意选择和同构不变逻辑的算法之间的不匹配。克服这个问题的一种方法是见证了对称的选择。它允许从可定义的轨道中进行选择，这些轨道通过可定义的见证自动形态认证。 我们考虑使用与对称选择（IFPC+WSC）进行计数（IFPC）的定点逻辑的扩展，并使用解释操作员（IFPC+WSC+i）进行进一步的扩展。后一个操作员在解释定义的结构中评估了一个子形式。该结构可能具有WSC操作员可利用的其他自动形态。对于纯固定点逻辑（IFP）的类似扩展，已知IFP+WSCI模拟了计数IFP+WSC无法做到的。对于IFPC+WSC，尚不清楚解释操作员是否会提高表现力，从而允许研究WSC与超出计数的解释之间的关系。 我们通过显示IFPC+WSC在FO解释下未关闭IFPC+WSC与IFPC+WSCI分开。通过同样的论点，我们回答了Dawar和Richerby关于IFP中非态度对称选择的一个公开问题。此外，我们证明使用所谓的CFI图可以提高嵌套WSC-oserators提高表现力。我们表明，如果IFPC+WSC+i会容顾特定的基本图，那么它还容顾相应的CFI图。这不同于其他各种逻辑，其中CFI图提供了困难的实例。
At the core of the quest for a logic for PTime is a mismatch between algorithms making arbitrary choices and isomorphism-invariant logics. One approach to overcome this problem is witnessed symmetric choice. It allows for choices from definable orbits which are certified by definable witnessing automorphisms. We consider the extension of fixed-point logic with counting (IFPC) with witnessed symmetric choice (IFPC+WSC) and a further extension with an interpretation operator (IFPC+WSC+I). The latter operator evaluates a subformula in the structure defined by an interpretation. This structure possibly has other automorphisms exploitable by the WSC-operator. For similar extensions of pure fixed-point logic (IFP) it is known that IFP+WSCI simulates counting which IFP+WSC fails to do. For IFPC+WSC it is unknown whether the interpretation operator increases expressiveness and thus allows studying the relation between WSC and interpretations beyond counting. We separate IFPC+WSC from IFPC+WSCI by showing that IFPC+WSC is not closed under FO-interpretations. By the same argument, we answer an open question of Dawar and Richerby regarding non-witnessed symmetric choice in IFP. Additionally, we prove that nesting WSC-operators increases the expressiveness using the so-called CFI graphs. We show that if IFPC+WSC+I canonizes a particular class of base graphs, then it also canonizes the corresponding CFI graphs. This differs from various other logics, where CFI graphs provide difficult instances.
