License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2022.23
URN: urn:nbn:de:0030-drops-157433
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/15743/
Go to the corresponding LIPIcs Volume Portal

Hazard, Emile ; Kuperberg, Denis

Cyclic Proofs for Transfinite Expressions

pdf-format:
LIPIcs-CSL-2022-23.pdf (0.8 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{hazard_et_al:LIPIcs.CSL.2022.23,
  author =	{Hazard, Emile and Kuperberg, Denis},
  title =	{{Cyclic Proofs for Transfinite Expressions}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/15743},
  URN =		{urn:nbn:de:0030-drops-157433},
  doi =		{10.4230/LIPIcs.CSL.2022.23},
  annote =	{Keywords: transfinite expressions, transfinite automata, cyclic proofs}
}

Keywords: transfinite expressions, transfinite automata, cyclic proofs
Collection: 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
Issue Date: 2022
Date of publication: 27.01.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI