2026-07-24T10:25:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18185 2024-03-06T11:01:15Z ddc:004 open_access

Witnessed Symmetric Choice and Interpretations in Fixed-Point Logic with Counting Lichter, Moritz witnessed symmetric choice interpretation fixed-point logic counting CFI graphs logic for PTime 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 tackle this problem is witnessed symmetric choice. It allows for choices from definable orbits 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. When similarly extending pure fixed-point logic (IFP), IFP+WSC+I 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. In this paper, we separate IFPC+WSC from IFPC+WSC+I 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Moritz Lichter 2023 Is Part Of LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2023.133 urn:nbn:de:0030-drops-181858 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.133 eng https://creativecommons.org/licenses/by/4.0/legalcode