Sergei Artemov and Elena Nogina

From Logic of Proofs to Evidence-Based Logics of Knowledge

The issue of a logic of knowledge with justifications, which we call here "evidence-based knowledge", has been discussed since the early 1990s. Such a logic along with the usual knowledge operator K_i(F) "agent i knows F" should contain assertions t:F, "t is an evidence of F". Starting from logics of proofs and provability we built basic systems of evidence-based knowledge, give their epistemic semantics (with a substantial contribution by Mel Fitting) and establish a number of their fundamental properties reflecting the explicit character of knowledge captured by those systems. We show that the evidence-based knowledge represents a stronger and more flexible version of the common knowledge operator. Evidence-based knowledge is free of logical omniscience, model-independent, has natural motivation and semantics. Furthermore, evidence-based knowledge can be presented by normal multi-modal logics, which places it in the scope of well-developed machinery applicable to modal logic: models, normalized proofs, automated proof search, complexity bounds, etc.