中央研究院 資訊科學研究所

The realization theorem connects justification logic with modal epistemic logic with the implication that there is indeed a  justification structure beneath every epistemic theorem which is concealed in the epistemic formalism. In this paper, we will give an alternative proof procedure for the realization theorem. By a strong theorem, we mean an epistemic theorem whose realization is a theorem in  justification logic without + involved. We will show that every epistemic theorem has a related strong theorem and then provide an algorithmic procedure turning the realization of the related strong theorem to the realization of the target epistemic theorem. We prove the existence of the related strong theorems both by a semantic method and by a constructive method.