  In this paper we present analytic tableau proof systems for various
justification logics. We show that the tableau systems are sound and complete
with respect to Mkrtychev models. In order to prove the completeness of the
tableaux, we give a syntactic proof of cut elimination. We also show the
subformula property for our tableaux, and prove the decidability of
justification logics for finite constant specifications.
