Quantum mechanics

Sequent calculus

Proof theory

Pure mathematics

Discrete mathematics

Kleene algebra

Computer science

Physics

Mathematics

Mathematical proof

Structural proof theory

Geometry

Action (physics)

Sequent

Algebra over a field

HAL (Le Centre pour la Communication Scientifique Directe)

We prove cut-elimination for a sequent-style proof system which is sound and complete for the equational theory of Kleene algebra, and where proofs are (potentially) non-wellfounded infinite trees. We extend these results to systems with meets and residuals, capturing `star-continuous' action lattices in a similar way. We recover the equational theory of all action lattices by restricting to regular proofs (with cut) - those proofs that are unfoldings of finite graphs.

Non-wellfounded proof theory for (Kleene+action)(algebras+lattices)