3 papers
cs.LO2020
Canonization for Bounded and Dihedral Color Classes in Choiceless Polynomial Time
Moritz Lichter, Pascal Schweitzer
In the quest for a logic capturing PTime the next natural classes of structures to consider are those with bounded color class size. We present a canonization procedure for graphs…
cs.LO2019
Walk refinement, walk logic, and the iteration number of the Weisfeiler-Leman algorithm
Moritz Lichter, Ilia Ponomarenko, Pascal Schweitzer
We show that the 2-dimensional Weisfeiler-Leman algorithm stabilizes n-vertex graphs after at most O(n log n) iterations. This implies that if such graphs are distinguishable in 3-…
cs.LO2018
Constructive Analysis of S1S and Büchi Automata
Moritz Lichter, Gert Smolka
We study S1S and Büchi automata in the constructive type theory of the Coq proof assistant. For UP semantics (ultimately periodic sequences), we verify Büchi's translation of formu…