Towards completeness via proof search in the linear time -calculus: the case of Büchi inclusions

DOI10.1145/2933575.2933598zbMATH Open1401.68193OpenAlexW2529880865MaRDI QIDQ4635894FDOQ4635894

Lucca Hirschi, David Baelde, Amina Doumane, Alexis Saurin

Publication date: 23 April 2018

Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2933575.2933598

Recommendations

• Constructive completeness for the linear-time \(\mu \)-calculus
• A Proof System for the Linear Time μ-Calculus
• Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics
• scientific article; zbMATH DE number 7297836
• On the proof theory of the modal mu-calculus

zbMATH Keywords

mu-calculussequent calculusparity automataproof-searchcircular proofs(co)inductionSafra construction

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Structure of proofs (03F07)

Cited In (6)

• Complete axiomatization of the stutter-invariant fragment of the linear time \(\mu\)-calculus
• Title not available (Why is that?)
• Non-well-founded deduction for induction and coinduction
• Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs
• A Buchholz rule for modal fixed point logics
• Title not available (Why is that?)

This page was built for publication: Towards completeness via proof search in the linear time \(\mu\)-calculus: the case of Büchi inclusions

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