The central open question in Descriptive Complexity is whether there is a logic that characterizes deterministic polynomial time (PTIME) on relational structures. Currently, a characterization of PTIME is known for linearly ordered structures only. For arbitrary  structures, capturing PTIME remains an intriguing open problem, that, so far, has resisted any attempt to solve it. 

In a related area of Constraint Satisfaction problem, a much more significant progress has been made. The long-standing Fedor-Vardi dichotomy conjecture has been resolved by Bulatov and Zhuk in 2017. 

The CSP development relied on Universal-algebraic techniques. Unfortunately, those techniques cannot be used in the current approaches in Descriptive Complexity. In particular, explicit counting constructs, that are used in several approaches to the problem, are an obstacle toward algebraization. 

We develop an algebraic approach to the problem. We define an algebra that is obtained from first-order logic with fixed points, FO(FP), by a series of transformations that include restricting logical connectives. The algebra is, simultaneously, a modal Dynamic logic where programs (or proofs) appear inside the modalities. The idea is to allow the logic to express exactly NP, and then use algebraic techniques to find syntactic conditions for PTIME. 

We describe the difficulties of building a bridge to Universal algebra, and introduce a proof system towards this goal.