Research On Justification Logic

The notion of justification is an important part in research of cognition since Plato. Plato has three criteria for knowledge:justification, truth and belief, however, though researchers of logic manage belief and truth in formal logic model of knowledge and belief, justification still lack management, justification is introduced into logic model of knowledge only after the emerge of justification logic.Godel speak about justification logic in1938, Artemov and Strassen give the prototype of the logic of proofs, Artemov gives LP, the logic of proofs, for the first time in1994, and gives the logic of proofs completely formally and relatively systematically in2001, from this we could get many new justification systems. The first normal possible world model for justification logic is Mkrtyclicv model, which is given by Mkrtychev in1997, Fitting gives the possible world model for LP normally in2005, there are other models such as modular model, minimal model, etc. The problem of conservative extension for justification logic is also an important question.Yavorskaya puts provability logic GL and LP together and gets LPP, Artemov and Nogina gives the axiomation of GLA, they also do research on system S4LP and S4LPN, which contain both classic modal operator and justification. Artemov introduces evidence-based knowledge, then gets evidence-based knowledge system based on multi-agent logic of knowledge, he gives justified knowledge system TnJ, S4nJ and S5nJ, which are the counterpart of TnLP, S4nLP and S5nLP, respectively. There are also research on hybrid-JT, denial logic, and justified descriptive logic. We give a resolution to the Muddy Children Puzzle through T3.Fitting gives QLP, Dean and Kurokawa analyze The Knower Paradox using QLP, but Arlo-Costa and Kishida object to this analyzation. Quantified Fitting model is got by adding first order quantification machinery based on Fitting model for LP, Artemov and Yavorskaya give first-order logic of proofs, Fitting gives possible world model for FOLP based on Fitting model for LP. We get a new system QLP, which is easier and more natural than QLP.The tableaux system for LP is first given by Renne in2004, Fitting gives a tableaux system for S4LP, Renne gives another tableaux system for LP and S4LP afterwards, Finger gives two analytic tableaux system KELP and preKELP for LP, Kurokawa gives a prefixed tableaux system TS4LPN for S4LPN, Fitting gives a prefixed tableaux system for K+J, S4LP, S4LPN, and S5LPN.Artemov gives the notion of realization and the algorithm of realization for LP in1995. Brezhnev and Kuznets give an algorithm of realization in which the proof polynomial is at most quadratic in length, Fitting gives a machinery in which we could reason with justification directly, Briinnler, Goetschi, and Kuznets prove a syntactic realization theorem, Goetschi and Kuznets then give a more general, constructive method of proving realization theorem, and give uniform realization theorem, Fitting gives a new algorithm of realization for LP based on tableaux system, and gives a Prolog implementation program of it. We extend Fitting’s algorithm of realization to the circumstance of FOLP, and prove the correctness of the algorithm of quasi-realization to realization of FOLP in detail.Justification logic stems from many theories such as mainstream epistemology, mathematical logic, computer science, artificial intelligence, etc. It absorbs basic principles of mainstream epistemology and proof theory, provides an arithmetical semantics to intuitionistic logic and a new semantics based on evidence to the logic of knowledge. The emerge of justification logic solves some problems:Godel’s provability semantics for classic modal system S4, formalization of BHK semantics for intuitionistic propositional logic, the notion of justification in epistemic logic in the model of knowledge. It makes the expressive power of epistemic logic more powerful, justification terms also provide natural measure machinery to the complexity of justification logic. Now, the research of justification logic is still very active, justification logic has much to improve, research, and develop.