On realization of S5-modality by evidence terms
We introduce a logic of evidence-based knowledge S5(n)LP(S5)in which the evidence part is based on logic of proofs with negative checker LP(S5). The later is obtained from the Logic of proofs LP by adding a new unary operation of negative checker '?' and the corresponding axiom. We define Kripke-style models for S5(n)LP(S5) and prove the completeness with respect to this semantics. We also define the logic of justified knowledge for S5(n)LP(S5).
logic of evidence-based knowledge logic of proofs logic of proofs with negative checker epistemic modal logic s5