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

DOI10.1145/2933575.2933598MaRDI QIDQ4635894zbMATH OpenOpenAlexFDO

Authors Amina Doumane, David Baelde, Lucca Hirschi, 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

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)

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

Cited in

(8)

• Complete axiomatization of the stutter-invariant fragment of the linear time \(\mu\)-calculus
• scientific article; zbMATH DE number 7155168 (Why is no real title available?)
• A Proof System for the Linear Time μ-Calculus
• Constructive completeness for the linear-time \(\mu \)-calculus
• Local validity for circular proofs in linear logic with fixed points
• 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

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)