English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

The central open question in Descriptive Complexity is whether there is alogic that characterizes deterministic polynomial time (PTIME) on relationalstructures. Towards this goal, we define a logic that is obtained fromfirst-order logic with fixed points, FO(FP), by a series of transformationsthat include restricting logical connectives and adding a dynamic version ofHilbert's Choice operator Epsilon. The formalism can be viewed, simultaneously,as an algebra of binary relations and as a linear-time modal dynamic logic,where algebraic expressions describing ``proofs'' or ``programs'' appear insidethe modalities. We show how counting, reachability and ``mixed'' examples (thatinclude linear equations modulo two) are axiomatized in the logic, and how anarbitrary PTIME Turing machine can be encoded. For each fixed Choice function,the data complexity of model checking is in PTIME. However, there can beexponentially many such functions. A crucial question is under what syntacticconditions on algebraic terms checking just one Choice function is sufficient.Answering this question requires a study of symmetries among computations. Thispaper sets mathematical foundations towards such a study via algebraic andautomata-theoretic techniques.

Towards Capturing PTIME with no Counting Construct (but with a Choice Operator)