A Proof System for the Linear Time μ-Calculus
DOI10.1007/11944836_26zbMATH Open1163.03308OpenAlexW1568149704MaRDI QIDQ5385992FDOQ5385992
Christian Dax, Martin Lange, Martin Hofmann
Publication date: 17 April 2008
Published in: FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11944836_26
Recommendations
- Constructive completeness for the linear-time \(\mu \)-calculus
- scientific article; zbMATH DE number 2102740
- Towards completeness via proof search in the linear time \(\mu\)-calculus: the case of Büchi inclusions
- From linear time to branching time
- Satisfiability of linear time mu-calculus on finite traces
Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Logic in computer science (03B70) Complexity of proofs (03F20)
Cited In (25)
- Loop-type sequent calculi for temporal logic
- Title not available (Why is that?)
- Complete axiomatization of the stutter-invariant fragment of the linear time \(\mu\)-calculus
- Verification, Model Checking, and Abstract Interpretation
- Title not available (Why is that?)
- Coinduction in Flow: The Later Modality in Fibrations
- Cyclic hypersequent system for transitive closure logic
- Certifying proofs for SAT-based model checking
- Size-Change Termination and Satisfiability for Linear-Time Temporal Logics
- Loop-check specification for a sequent calculus of temporal logic
- Ramsey-Based Inclusion Checking for Visibly Pushdown Automata
- On the proof theory of the modal mu-calculus
- Satisfiability of Linear Time Mu-Calculus on Finite Traces
- Two Ways to Common Knowledge
- Non-well-founded deduction for induction and coinduction
- Cyclic implicit complexity
- Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs
- The Proof Theory of Common Knowledge
- A focus system for the alternation-free \(\mu \)-calculus
- Circular (Yet Sound) Proofs in Propositional Logic
- A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points
- Ill-founded proof systems for intuitionistic linear-time temporal logic
- Cyclic Arithmetic Is Equivalent to Peano Arithmetic
- Title not available (Why is that?)
- Title not available (Why is that?)
This page was built for publication: A Proof System for the Linear Time μ-Calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5385992)
