On global induction mechanisms in aμ-calculus with explicit approximations

DOI10.1051/ITA:2003024MaRDI QIDQ4460690zbMATH OpenOpenAlexFDO

Authors Christoph Sprenger, Mads Dam

Publication date 29 March 2004

Published in RAIRO - Theoretical Informatics and Applications (Search for Journal in Brave)

Full work available at URL http://www.numdam.org/item?id=ITA_2003__37_4_365_0, https://eudml.org/doc/92728

zbMATH Keywords

inductive reasoning

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1956528
• Automated Reasoning with Analytic Tableaux and Related Methods
• On the proof theory of the modal mu-calculus
• -Calculus with Explicit Points and Approximations
• Publication:4938644

Cites work

• -Calculus with Explicit Points and Approximations
• Finiteness is mu-ineffable
• Games for the -calculus
• scientific article; zbMATH DE number 1142314 (Why is no real title available?)
• scientific article; zbMATH DE number 1956528 (Why is no real title available?)
• scientific article; zbMATH DE number 2087443 (Why is no real title available?)
• Local model checking for infinite state spaces
• Local model checking in the modal mu-calculus
• Modalities for model checking: Branching time logic strikes back
• Proving properties of dynamic process networks
• Results on the propositional \(\mu\)-calculus

Cited in

(12)

• Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS
• Extracting proofs from tabled proof search
• Cyclic arithmetic is equivalent to Peano arithmetic
• scientific article; zbMATH DE number 1956528 (Why is no real title available?)
• scientific article; zbMATH DE number 956830 (Why is no real title available?)
• From GTC to \textsc{Reset}: generating reset proof systems from cyclic proof systems
• Cyclic proofs for the first-order -calculus
• Abstract cyclic proofs
• A sequent calculus for trace formula implication
• Proof systems for two-way modal -calculus
• Trace-based deductive verification
• Computation by infinite descent made explicit

This page was built for publication: On global induction mechanisms in aμ-calculus with explicit approximations

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