Certification of labeled proofs for modal logics with geometric frame conditions

Several proof formalisms have been used, and in some cases even introduced, in order to define proof systems for modal logic. Our work falls within a more general project of establishing a common specification language for checking proofs given in a wide range of deductive formalisms. In this paper, we consider the case of labeled proof systems for modal logics, i.e., in particular, Negri's labeled se-quent calculi, Fitting's prefixed tableaux and free-variable prefixed tableaux, and provide a framework for certifying proofs given in such calculi. The method is based on the use of a translation from the modal language into a first-order polarized language and on a checker whose trusted kernel is a simple implementation of a classical focused sequent calculus. The framework allows for a high flexibility in the representation of proofs to be checked, in the sense that even partial proofs can be verified by employing a process of proof reconstruction. We describe the general method for modal logics characterized by geometric frame conditions, present its implementation in a Prolog-like language, and provide several examples of proof certification in the case of well-known normal modal logics, like K, S4 and S5.