A cut-free cyclic proof system for kleene algebra

Anupam Das, Damien Pous

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

12 Citations (Scopus)
85 Downloads (Pure)

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.

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
PublisherSpringer
Pages261-277
ISBN (Electronic)9783319669021
ISBN (Print)9783319669014
DOIs
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
Country/TerritoryBrazil
CityBrasilia
Period25/09/1728/09/17

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'A cut-free cyclic proof system for kleene algebra'. Together they form a unique fingerprint.

Cite this