There will be three parts in this thesis. The first part is a survey of epistemic logic. Epistemic logic was first introduced by philosophers, and later found its applications in fields such as Computer Science and Economics. The survey will cover both the philosophical debates and applications of epistemic logic, and then discussions of the logical omniscience problem will follow.

The second part is the introduction of a new logical framework timed Modal Epistemic Logic. tMEL. tMEL is extended from ordinary modal epistemic logic, MEL, by adding numerical labels to knowledge statement to indicate when the statement is known. We will argue how a logical framework reasoning about both knowledge and the time of reasoning can help to resolve the problem of logical omniscience, and tMEL serves well as a logically non-omniscient epistemic system.

Finally, we will discuss the syntactical relations between MEL, tMEL, and Justification Logic, from which the study of MEL is originated. Our focus will be on the relations between axiomatic proofs of these logical frameworks. We will first determine a proper subclass of modal logical proofs called non-circular, and prove that this class of proofs is complete. And then we will show that every non-circular MEL proof can be turned into a tMEL proof by finding suitable number labels, and prove that there is a two-way translation between proofs in tMEL and Justification Logic. Combining these results, a formal connection between non-circular proofs and proofs in Justification Logic is established, and the whole procedure gives us an alternative algorithm for the realization between theorems in modal logic and Justification Logic. This is the end of the abstract.