ABSTRACT:
Justification logics provide a framework for reasoning about epistemic justifications. In this thesis we study justification logics and their relations with modal logics. The results of the thesis can be divided into two parts: we introduce new justification logics and prove the realization theorem, and study the proof theory of justification logics. We introduce new justification logics JB (justification counterpart of Browerean modal logic KB) and its extensio JGL (justification counterpart of G?del-L?b provability logic GL); JKnD, JTnD, JS4nD , and JS5nD (justification counterpart of distributed knowledge logics LD). For these justification logics the realization theorem are proved, epistemic models are given and completeness theorems are established. We prove the realization theorem for KB using embedding in another justification logic, for GL using Artemov’s syntactical method, and for LD using Fitting’s semantical method. We also provide various proof systems for justification logics and prove the cut elimination theorem for most of them. We present a syntactical proof of cut elimination for Artemov's sequent calculus LPG of the logic of proofs LP, and present cut-free sequent calculi LPG and LPLG for the logic of proofs, cut-free sequent calculi S4LPG and S4LPLG for epistemic logic with justification S4LP, cut-free hypersequent calculus S4LPNLH for epistemic logic with justification S4LPN, cut- and contraction-free labeled sequent calculus for most of the justification logics as well as S4LP and S4LPN.