modal-logics

Agda formalisation associated to the paper "Dual-context Calculi for Modal Logic." A preprint can be found at

https://arxiv.org/abs/1602.04860

Contains basic metatheoretic results about dual-context calculi (e.g. admissibility of weakening, contraction, cut) as well as proofs of equivalence with the relevant Hilbert systems (up to provability only).