Cyclic Proofs and Jumping Automata
Denis Kuperberg, Laureline Pinault, Damien Pous · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2019
We consider a fragment of a cyclic sequent proof system for Kleene algebra, and we see it as a computational device for recognising languages of words. The starting proof system is linear and we show that it captures precisely the regular languages. When adding the standard contraction rule, the expressivity raises significantly; we characterise the corresponding class of languages using a new notion of multi-head finite automata, where heads can jump.