A cut-free cyclic proof system for Kleene algebra

DOI10.1007/978-3-319-66902-1_16MaRDI QIDQ1694471zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(16)

• scientific article; zbMATH DE number 515726 (Why is no real title available?)
• Uniform interpolation from cyclic proofs: the case of modal mu-calculus
• scientific article; zbMATH DE number 7561320 (Why is no real title available?)
• scientific article; zbMATH DE number 7533344 (Why is no real title available?)
• Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
• scientific article; zbMATH DE number 7155168 (Why is no real title available?)
• 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

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)