A cut-free cyclic proof system for Kleene algebra

DOI10.1007/978-3-319-66902-1_16zbMath1496.03229OpenAlexW2726021294MaRDI QIDQ1694471

Damien Pous, Anupam Das

Publication date: 2 February 2018

Full work available at URL: http://pure-oai.bham.ac.uk/ws/files/81094094/A_cut_free.pdf

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05)

Related Items (9)

Uniform interpolation from cyclic proofs: the case of modal mu-calculus ⋮ Unnamed Item ⋮ Cyclic hypersequent system for transitive closure logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent ⋮ Non-well-founded deduction for induction and coinduction ⋮ Cyclic proofs, hypersequents, and transitive closure logic ⋮ Loop-check specification for a sequent calculus of temporal logic

This page was built for publication: A cut-free cyclic proof system for Kleene algebra