While modal logic has been a standard approach for reasoning about knowledge and belief of intelligent agents [7, 11] since the seminal work by Hintikka [10], the notion of justification, which is an essential component in Plato's tripartite definition of knowledge as justified true belief, was largely ignored in the formalisms. Because the formula □Φ is interpreted as "Φ is believable" or "Φ is knowable" in the epistemic/doxastic reading of modal logics, explicit justifications are not represented in the logic. By contrast, justification logics (JL) supply the missing component by adding justification terms to epistemic formulas [5, 2, 4, 8]. The first member of the JL family is the logic of proofs (LP) proposed in [1]. Although the original purpose of LP is to formalize the Brouwer-Heyting-Kolmogorov semantics for intuitionistic logic and establish the completeness of intuitionistic logic with respect to this semantics, in a more general setting, JL has evolved into a kind of explicit epistemic logic and received much attention in computer science and AI [2, 5].
展开▼
