2026-07-23T05:45:59Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11607 2024-03-06T10:48:26Z ddc:004 open_access

Cyclic Proofs and Jumping Automata Kuperberg, Denis Pinault, Laureline Pous, Damien Cyclic proofs regular languages multi-head automata transducers 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Denis Kuperberg and Laureline Pinault and Damien Pous 2019 Is Part Of LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2019.45 urn:nbn:de:0030-drops-116071 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.45 eng https://creativecommons.org/licenses/by/3.0/legalcode