On non-self-referential realizable fragments
CUNY Graduate Center
Given the known fact that realizations of modal logics T, K4, S4, and intuitionistic propositional logic IPC (via S4) each requires justification formula that is self-referential, it is reasonable to consider the fragment of each that can be realized non-self-referentially, called the non-self-referential realizable (NSR) fragment. Based on prehistoric graphs of G3-style sequent proofs of modal theorems, we are able to define the loop-free-provable (LFP) fragment of each logic that turns out to be a decidable subset of the NSR fragment. In this talk, we will explore properties of LFP fragments, their applications in the study of NSR fragments, and other related issues.
Junhua Yu is a Ph.D. student of Computer Science in the Graduate Center under supervision of Sergei Artemov. Junhua is a winner of the Yandex Best Paper Award for the best student paper from the 5th International Computer Science Symposium in Russia, CSR 2010, and the Rosser Prize for the best student paper from the Symposium on Logical Foundations of Computer Science 2013 in San Diego.