Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski
From MaRDI portal
Publication:4953222
DOI10.2307/2586539zbMath0982.03011OpenAlexW2057072590MaRDI QIDQ4953222
Marco Hollenberg, Giovanna D'Agostino
Publication date: 14 June 2000
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2586539
interpolationmodal mu-calculusLoś-Tarski theoremLyndon theoremclassical theorems of model theorymu-automata
Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Interpolation, preservation, definability (03C40) Other classical first-order model theory (03C68)
Related Items
On modal logics of model-theoretic relations, A note on constructive interpolation for the multi-modal logic \(K_m\), The mu-calculus and Model Checking, Uniform interpolation from cyclic proofs: the case of modal mu-calculus, Model theory of monadic predicate logic with the infinity quantifier, Unnamed Item, On the Notion of Vacuous Truth, Knowledge forgetting in propositional \(\mu\)-calculus, Deciding the existence of uniform interpolants over transitive models, Modal frame correspondences and fixed-points, A decidability result for the model checking of infinite-state systems, Coalgebraic semantics of modal logics: an overview, Unnamed Item, The Lyndon property and uniform interpolation over the Grzegorczyk logic, Continuous Fragment of the mu-Calculus, Refinement modal logic, Bisimulation quantifiers and uniform interpolation for guarded first order logic, Completeness for \(\mu\)-calculi: a coalgebraic approach, Uniform interpolation and coherence, Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics, Semantics for knowledge and change of awareness, Ambiguous classes in \(\mu\)-calculi hierarchies, An axiomatization of bisimulation quantifiers via the \(\mu\)-calculus, On modal \(\mu\)-calculus with explicit interpolants, Interpolation properties for provability logics GL and GLP, 2004 Summer Meeting of the Association for Symbolic Logic, Positive announcements, Fixed-Point Elimination in the Intuitionistic Propositional Calculus, $$\mu $$ μ -Levels of Interpolation, The many faces of interpolation, Interpolation in non-classical logics, Unnamed Item, Craig Interpolation for Linear Temporal Languages, μ-programs, uniform interpolation and bisimulation quantifiers for modal logics ★, Forgetting in multi-agent modal logics, Combination of uniform interpolants via Beth definability, On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions
Cites Work
- Properties preserved in subdirect products
- An automata theoretic decision procedure for the propositional mu- calculus
- Propositional dynamic logic of regular programs
- Modalities for model checking: Branching time logic strikes back
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- “Sometimes” and “not never” revisited
- On an interpretation of second order quantification in first order intuitionistic propositional logic
- Temporal logics of “the next” do not have the beth property
