Tableaux and hypersequents for justification logics (Q408538)

Logics of proofs (now called justification logics), introduced by S. Artemov, are usually based on S4. The author investigates a system S4LPN, introduced by S. Artemov and E. Nogina, which has an additional S5-like schema. He presents rather complicated tableau and hypersequent formulations for S4LPN. It is possible that a much more elegant formulation can be obtained using a cut-free system for S5 due to \textit{G. F. Shvarts} [``Gentzen style systems for K45 and K45D'', Lect. Notes Comput. Sci. 363, 245--256 (1989; Zbl 0677.03010)].