+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Mittwoch, 12. Juli 2023, 11:00 Uhr Ort: Informatikzentrum der RWTH Aachen University, Gebäude E3, 2. Etage, Raum 9222 Referent: Benedikt Pago, M.Sc. Mathematische Grundlagen der Informatik Thema: Limitations of Choiceless Computation Abstract: A central open question in finite model theory asks whether there exists a logic that captures the complexity class PTIME. Another way of phrasing this is whether every polynomial time algorithm can be efficiently simulated by a choiceless one. Choiceless computation models operate on finite structures, such as graphs, and can only perform computation steps which are invariant under the symmetries of the structure. This guarantees that for any two isomorphic input structures, the outcome of the computation is the same - a property which is typically required of logics. The quest for a logic for PTIME seeks to develop and analyse logics (i.e. choiceless computation models) of increasing expressive power within PTIME. One of the most prominent logics that has been suggested and not separated from PTIME within more than 20 years is Choiceless Polynomial Time (CPT). Obtaining a better understanding of its expressive power is the aim of this thesis; the focus is on its limitations, since only little is known so far in this regard. We develop new approaches and techniques towards strong CPT lower bounds. As a promising candidate for separating CPT from PTIME, we propose the graph isomorphism problem on Cai-Fürer-Immerman (CFI) graphs over unordered hypercubes. The CFI construction is a well-known tool to prove inexpressibility results for logics. Choiceless polynomial time algorithms are known to exist for certain ordered variants of it but we show that these fail on unordered CFI graphs. Going further, we study a broader class of CPT-algorithms for this problem and prove that lower bounds against certain families of symmetric Boolean circuits imply lower bounds for these algorithms. A first lower bound for this kind of circuits is also presented to demonstrate the feasibility of the approach. It remains open to strengthen it further to get the desired undefinability result for the CFI problem in CPT. 
As an alternative route, we establish a connection to an algebraic proof system called the extended polynomial calculus. The power of this and similar proof systems is the subject of active research in the field of proof complexity. We show that suitable proof complexity lower bounds would imply the separation of CPT and PTIME, too. Es laden ein: die Dozentinnen und Dozenten der Informatik