A cut-free cyclic proof system for Kleene algebra

DOI10.1007/978-3-319-66902-1_16zbMATH Open1496.03229OpenAlexW2726021294MaRDI QIDQ1694471FDOQ1694471

Authors: Anupam Das, Damien Pous 

Publication date: 2 February 2018

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

Recommendations

• Left-Handed Completeness for Kleene algebra, via Cyclic Proofs
• Automatic Proof Generation in Kleene Algebra
• On regular expression proof complexity
• A completeness theorem for Kleene algebras and the algebra of regular events
• Kleene algebra with converse

Mathematics Subject Classification ID

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

Cited In (16)

• Uniform interpolation from cyclic proofs: the case of modal mu-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
• Title not available (Why is that?)
• Left-Handed Completeness for Kleene algebra, via Cyclic Proofs
• Cyclic hypersequent system for transitive closure logic
• Loop-check specification for a sequent calculus of temporal logic
• Non-well-founded deduction for induction and coinduction
• On regular expression proof complexity
• Cyclic implicit complexity
• Automatic Proof Generation in Kleene Algebra
• A complete inference system for skip-free guarded Kleene algebra with tests
• Cyclic proofs, hypersequents, and transitive closure logic
• Cyclic proofs for transfinite expressions
• Title not available (Why is that?)

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1694471)