When: Thursday, November 18, 2021, 3pm (CEST).

Where: Zoom online & Aula Magna at DIAG, check the address in the Google Calendar Event.

Topic: Towards Capturing PTIME with no Counting Construct (but with a version of Hilbert’s Choice operator).

Speaker: Prof. Eugenia Ternovska, Associate Professor at Simon Fraser University, Vancouver, Canada.

Abstract

The central open question in Descriptive Complexity is whether there is a logic that characterizes deterministic polynomial-time computations (PTIME) on relational structures. In this talk, I introduce my work on this question. I define an algebra of binary relations that is obtained from first-order logic with fixed points, FO(FP), by a series of transformations that include restricting logical connectives and adding a dynamic version of Hilbert’s Choice operator Epsilon. The formalism can also be viewed as a linear-time modal Dynamic logic, where algebraic expressions describing “proofs” or “programs” appear inside the modalities. Many typical polynomial-time properties such as cardinality, reachability and those requiring “mixed” propagations (that include linear equations modulo two) can be specified in the logic, and an arbitrary PTIME Turing machine can be encoded. For each fixed Choice function, the data complexity of model checking is in PTIME. However, there can be exponentially many such functions. “Naive evaluations” refer to a version of this model checking procedure where the Choice function variable Epsilon is simply treated as a constant. A crucial question is under what syntactic conditions on the algebraic terms such a naive evaluation works, that is, provides a certain answer to the original model checking problem. These conditions, applied to the formalism, would give us a logic for PTIME. The two views of the formalism, as an algebra and as a Dynamic logic, support application of both automata-theoretic and algebraic techniques to the study of this question.

Short Bio

Eugenia Ternovska is an associate professor at Simon Fraser University, Vancouver, Canada. She obtained her PhD in 2002 in Artificial Intelligence under the supervision of Ray Reiter (1939-2002) at the University of Toronto, Canada. Her research is mainly about Logic in Computer Science, Descriptive Complexity, Theoretical Computer Science, Knowledge Representation, Efficient Reasoning, Reasoning about Actions, Modal Logics, Fixpoint logics.

Material