  The initial Justification Logic system, the Logic of Proofs  \(\mathsf{LP}\),  was introduced in 1995 in (Artemov 1995) (cf.  also (Artemov 2001)) where such basic properties as Internalization,  Realization, arithmetical completeness, were first established. \(\mathsf{LP}\) offered an intended provability semantics for Gödel’s provability logic  \(\mathsf{S4}\),  thus providing a formalization of Brouwer-Heyting-Kolmogorov semantics for intuitionistic propositional logic.  Epistemic semantics and completeness (Fitting 2005) were first  established for \(\mathsf{LP}\).  Symbolic models and decidability for  \(\mathsf{LP}\)  are due to Mkrtychev (Mkrtychev 1997).  Complexity estimates first appeared in (Brezhnev and Kuznets 2006,  Kuznets 2000, Milnikel 2007). A comprehensive overview of all  decidability and complexity results can be found in (Kuznets 2008).  Systems \(\mathsf{J} , \mathsf{J4}\), and  \(\mathsf{JT}\)  were first considered in (Brezhnev  2001) under different names and in a slightly different setting.  \(\mathsf{JT45}\) appeared  independently in (Pacuit 2006) and (Rubtsova 2006), and  \(\mathsf{JD45}\) in (Pacuit 2006). The logic of uni-conclusion proofs has been found in (Krupski 1997).  A more general approach to common knowledge based on justified knowledge was offered in (Artemov 2006).  Game semantics of Justification Logic and Dynamic Epistemic Logic with  justifications were studied in (Renne 2008, Renne 2009). Connections  between Justification Logic and the problem of logical omniscience  were examined in (Artemov and Kuznets 2009, Wang 2009). The name Justification Logic was introduced in (Artemov 2008), in which Kripke, Russell, and Gettier examples were formalized; this formalization has been used for the resolution of paradoxes, verification, hidden assumption analysis, and eliminating redundancies.  In (Dean and Kurokawa 2009a), Justification Logic was used for the analysis of Knower and Knowability paradoxes. 