Mechanizing bisimulation theorems for relation-changing logics in Coq

DOI10.1007/978-3-030-38808-9_1zbMATH Open1496.03042OpenAlexW3000719559MaRDI QIDQ777873FDOQ777873

Authors: Raul Fervari, Francisco Trucco, Beta Ziliani 

Publication date: 8 July 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-38808-9_1

Recommendations

• Verification of dynamic bisimulation theorems in Coq
• Formalizing cut elimination of coalgebraic logics in Coq
• Mechanizing common knowledge logic using COQ
• Relation-changing modal operators
• Relation-changing logics as fragments of hybrid logics

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

Cited In (2)

• Verification of dynamic bisimulation theorems in Coq
• Coalgebraic Reasoning in Coq: Bisimulation and the λ-Coiteration Scheme

Uses Software

• Coq

This page was built for publication: Mechanizing bisimulation theorems for relation-changing logics in Coq

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