2026-07-22T21:35:23Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:15743 2024-03-06T10:56:05Z ddc:004 open_access

Cyclic Proofs for Transfinite Expressions Hazard, Emile Kuperberg, Denis transfinite expressions transfinite automata cyclic proofs We introduce a cyclic proof system for proving inclusions of transfinite expressions, describing languages of words of ordinal length. We show that recognising valid cyclic proofs is decidable, that our system is sound and complete, and well-behaved with respect to cuts. Moreover, cyclic proofs can be effectively computed from expressions inclusions. We show how to use this to obtain a Pspace algorithm for transfinite expression inclusion. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Emile Hazard and Denis Kuperberg 2022 Is Part Of LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2022.23 urn:nbn:de:0030-drops-157433 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.23 eng https://creativecommons.org/licenses/by/4.0/legalcode