Uniform interpolation from cyclic proofs: the case of modal mu-calculus
From MaRDI portal
Publication:2142087
DOI10.1007/978-3-030-86059-2_20OpenAlexW3197483185MaRDI QIDQ2142087
Bahareh Afshari, Guillermo Menéndez Turata, Graham E. Leigh
Publication date: 25 May 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-86059-2_20
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Bisimulation quantifiers and uniform interpolation for guarded first order logic
- An axiomatization of bisimulation quantifiers via the \(\mu\)-calculus
- Games for the \(\mu\)-calculus
- Interpolation in non-classical logics
- A cut-free cyclic proof system for Kleene algebra
- Realizability in cyclic proof: extracting ordering information for infinite descent
- Uniform interpolation and sequent calculi in modal logic
- Infinets: the parallel syntax for non-wellfounded proof-theory
- A non-wellfounded, labelled proof system for propositional dynamic logic
- Uniform interpolation and the existence of sequent calculi
- Circular proofs for the Gödel-Löb provability logic
- Temporal Logics in Computer Science
- Beth Definability in Expressive Description Logics
- Cyclic Arithmetic Is Equivalent to Peano Arithmetic
- Sequent calculi for induction and infinite descent
- Automata for the modal μ-calculus and related results
- A Tableau System for the Modal μ-Calculus
- On an interpretation of second order quantification in first order intuitionistic propositional logic
- Interpolation with Decidable Fixpoint Logics
- Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski
- Cyclic Proofs for Linear Temporal Logic
- Automated Reasoning with Analytic Tableaux and Related Methods
- Automatically verifying temporal properties of pointer programs with cyclic proof
