We extended the propositional logic and its semantics. More about modal logic can be found here. Modal logic brings in the notion of necessity (box) and possibility (diamond). We proved the soundness theorem for modal logic and some theorems.
Project is divided into several files.
The semantics is defined in Soundness.agda
where is also the soundness proof.