A circular proof system for the hybrid mu-calculus
Sebastian Enqvist
TL;DR
This paper introduces a circular, cut-free proof system for the hybrid mu-calculus, ensuring soundness and completeness, and utilizing names for fixpoint unfoldings similar to Stirling's approach.
Contribution
It develops a novel circular proof system for the hybrid mu-calculus that extends previous mu-calculus methods with new naming techniques.
Findings
The proof system is sound and complete.
It is circular and cut-free.
Uses names for fixpoint unfoldings.
Abstract
We present a circular and cut-free proof system for the hybrid mu-calculus and prove its soundness and completeness. The system uses names for fixpoint unfoldings, like the circular proof system for the mu-calculus previously developed by Stirling.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Mathematics, Computing, and Information Processing · Logic, Reasoning, and Knowledge