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

Recommendations

A cut-free cyclic proof system for Kleene algebra
On Action Logic: Equational Theories of Action Algebras
An infinitary sequent system for the equational theory of *-continuous action lattices
Left-Handed Completeness for Kleene algebra, via Cyclic Proofs
Algebraic aspects of cut elimination

Cites work

scientific article; zbMATH DE number 1696821 (Why is no real title available?)
scientific article; zbMATH DE number 6680140 (Why is no real title available?)
scientific article; zbMATH DE number 1215493 (Why is no real title available?)
scientific article; zbMATH DE number 549971 (Why is no real title available?)
scientific article; zbMATH DE number 7362722 (Why is no real title available?)
scientific article; zbMATH DE number 3316966 (Why is no real title available?)
scientific article; zbMATH DE number 3366846 (Why is no real title available?)
A calculational approach to mathematical induction
A completeness theorem for Kleene algebras and the algebra of regular events
A cut-free cyclic proof system for Kleene algebra
An efficient Coq tactic for deciding Kleene algebras
An infinitary sequent system for the equational theory of *-continuous action lattices
Automata, Languages and Programming
Complete systems of \(\mathcal B\)-rational identities
Concurrent Kleene Algebra
From semirings to residuated Kleene lattices
Infinitary proof theory: the multiplicative additive case
Kleene algebra with tests and Coq tools for while programs
Least and Greatest Fixpoints in Game Semantics
Linear logic
Logic Programming with Focusing Proofs in Linear Logic
Netkat, semantic foundations for networks
On Action Logic: Equational Theories of Action Algebras
On Hoare logic and Kleene algebra with tests
Proof Pearl: regular expression equivalence and relation algebra
Regular expression containment, coinductive axiomatization and computational interpretation
Residuated lattices. An algebraic glimpse at substructural logics
The Mathematics of Sentence Structure
Une condition impliquant toutes les identités rationnelles

Cited in

(12)

Uniform interpolation from cyclic proofs: the case of modal mu-calculus
Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps
Non-well-founded deduction for induction and coinduction
Cyclic implicit complexity
Complexity of a fragment of infinitary action logic with exponential via non-well-founded proofs
Kleene star, subexponentials without contraction, and infinite computations
A restricted fragment of the Lambek calculus with iteration and intersection operations
Circular proofs as session-typed processes: a local validity condition
A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points
Canonicity of proofs in constructive modal logic
Integrating induction and coinduction via closure operators and proof cycles
NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC

Describes a project that uses

Uses Software

NetKAT
Regular Sets

This page was built for publication: Non-wellfounded proof theory for (Kleene+action)(algebras+lattices)

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