Soundness-Preserving Fusion of Modal Logics in Coq

• Miguel Alfredo Nunes Unicamp
• Karina Girardi Roggia UDESC
• Paulo Henrique Torrens University of Kent

Abstract

This work presents the formal verification of the concept of fusion of modal logics in the Coq proof assistent, along with a proof of the preservation of soundness. Our formalization is based on previous work by da Silveira et al. that formalizes several normal modal systems using Coq and proves their soundness and weak completeness. We give a high level description of the base library, how we modified it to fit our needs, how we defined fusion and how we proved the transfer of soundness. Our definition allows for the fusion of any normal modal logics, with any amount of modalities, requiring no changes to the definitions in the library.