Sesión Lógica y Computabilidad (II)

Diciembre 14, 11:40 ~ 12:00

Bisimulation for Justification Logic in Coq

Hoffmann, Guillaume

\newcommand{\model}{\mathsf M} Justification Logic~\cite{artemov2008logic} is a family of logics resulting from a general interpretation of the Logic of Proofs (LP). Justification Logic makes an explicit analysis of assertions, compared with the implicit approach of traditional modal logic. In particular, Justification Logic {\bf S4LP}~\cite{artemov2005introducing}, integrates modal and justification operators in the same framework. Using this formalization, it is possible to express proofs of both modal and justification statements. The Coq proof assistant~\cite{coq} is a powerful tool to formally verify sophisticated proofs~(\emph{e.g.}, \cite{fourcolor:gonthier}). In~\cite{andrade17} the authors provide a formalization of the syntax and sematincs of {\bf S4LP} in Coq, together with an axiomatization for this logic. They also provide a proof in Coq of the soundness for such axiomatization. We aim at continuing this line of work, proposing a Coq proof for the intrincate invariance theorem under bisimulation for Justification Logic. We plan to use a definition of bisimulation close to the one given in~\cite{renne2006bisimulation}. One possible dificulty of this definition of bisimulation is that one condition involves mapping together the sets of evidences of bisimilar states. Indeed, Fitting's models for justification logic~\cite{fitting2005logic} contain a function $\mathcal{E} : Just \times Forms \mapsto \mathscr{P}(W)$ which provides the semantic condition for justification statements: $$\model, w \models t : \varphi, \mbox{ iff } w \in \mathcal{E}(t, \varphi), \mbox{ and for every $v \in W$ such that if $wRv$, then } \model, v \models \varphi$$ We can change the definition of Kripke-Fitting models so that we instead use a ``justification label'' function $\mathcal{E'} : W \mapsto \mathscr{P}(Just \times Forms)$. However, the set $\mathscr{P}(Just \times Forms)$ may be difficult to formalize in a Coq proof, therefore we would like to explore alternative definitions. Once this is done, possible future works will be proving the finite version of inverse result of the invariance theorem. That is, that finite Kripke-Fitting models that coincide on all {\bf S4LP} formulas are bisimilar. Finally, we also want to prove completeness of the provided axiomatization for {\bf S4LP}. \vspace{-.8em} \bibliographystyle{plain} \begin{thebibliography}{1} \vspace{-.75em} \bibitem{andrade17} J.~M. Andrade-Guzman and F.~Hernandez-Quiroz. \newblock Natural deduction and semantic models of justification logic {S4LP} in the proof assistant {Coq}. \newblock In {\em 17th Latin American Symposium on Mathematical Logic}, 2017. \bibitem{artemov2008logic} S.~Artemov. \newblock The logic of justification. \newblock {\em The Review of Symbolic Logic}, 1(4):477--513, 2008. \bibitem{artemov2005introducing} S.~Artemov and E.~Nogina. \newblock Introducing justification into epistemic logic. \newblock {\em Journal of Logic and Computation}, 15(6):1059--1073, 2005. \bibitem{fitting2005logic} M.~Fitting. \newblock The logic of proofs, semantically. \newblock {\em Annals of Pure and Applied Logic}, 132(1):1--25, 2005. \bibitem{fourcolor:gonthier} Georges Gonthier. \newblock Formal proof --- the four-color theorem. \newblock {\em Notices of the {AMS}}, 55(11):1382--93, 2008. \bibitem{renne2006bisimulation} B~Renne. \newblock Bisimulation and public announcements in logics of explicit knowledge. \newblock In {\em Proceedings of the Rationality and Knowledge Workshop}, 2006. \bibitem{coq} {The {Coq} Development Team}. \newblock {\em {The Coq Proof Assistant Reference Manual -- Version V8.4}}, 2012. \end{thebibliography}

Autores: Areces, Carlos / Fervari, Raul / Hoffmann, Guillaume / Ziliani, Beta.