A cut-free cyclic proof system for kleene algebra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Authors

Colleges, School and Institutes

External organisations

  • Université de Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP

Abstract

We introduce a sound non-wellfounded proof system whose regular (or ‘cyclic’) proofs are complete for (in)equations between regular expressions. We achieve regularity by using hypersequents rather than usual sequents, with more structure in the succedent, and relying on the discreteness of rational languages to drive proof search. By inspection of the proof search space we extract a PSpace bound for the system, which is optimal for deciding such (in)equations.

Details

Original languageEnglish
Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods
Subtitle of host publication26th International Conference, TABLEAUX 2017, Brasilia, Brazil, September 25-28 2017, Proceedings
EditorsClaudia Nalon, Renate A. Schmidt
Publication statusPublished - 30 Aug 2017
Event26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2017 - Brasilia, Brazil
Duration: 25 Sep 201728 Sep 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10501 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2017
CountryBrazil
CityBrasilia
Period25/09/1728/09/17