Realization theorem for epistemic logic with justification
0
조회
0
다운로드
0
인용
0
참고문헌
키워드
초록
Epistemic logic with justi cation, S4LP, is a combination of the modal epistemic logic S4 and the logic of proofs LP. This logic together with the modal knowledge operator F (F is known), contain in nitely many operators of the form t : F (t is a justi cation for F), where t is a term. In this paper, we rst introduce cut-free sequent calculus for S4LP, which is suitable for realization of S4LP. Then, by generalizing the Artemov's realization algorithm, we show that theorems of S4LP can be realized in LP.
Abstract
Epistemic logic with justi cation, S4LP, is a combination of the modal epistemic logic S4 and the logic of proofs LP. This logic together with the modal knowledge operator F (F is known), contain in nitely many operators of the form t : F (t is a justi cation for F), where t is a term. In this paper, we rst introduce cut-free sequent calculus for S4LP, which is suitable for realization of S4LP. Then, by generalizing the Artemov's realization algorithm, we show that theorems of S4LP can be realized in LP.
참고문헌 (5)
- S. Artemov, "Explicit provability and constructive semantics", Bulletin of Symbolic Logic, 7(1), pp.1~36 (2001)
- Logic of knowledge with justications from the provability per- spective, "S. Artemov", CUNY Ph.D. Program in Computer Science, ~, pp.Technical Report TR-2004011 (2004)
- S. Artemov, "Introducing justication into epistemic logic", Journal of Logic and Computation, 15(6), pp.1059~1073 (2005)
- M. Ghari, "Cut elimination and realization for epistemic logics with justication", Journal of Logic and Computation, Advance Access (2011)
- A. Troelstra, "Basic Proof Theory" (1996), Cambridge University Press