2 papers
math.LO2025
Cut-free sequent calculi for the provability logic D
Ryo Kashima, Taishi Kurahashi, Sohei Iwata +1
We say that a Kripke model is a GL-model if the accessibility relation is transitive and converse well-founded. We say that a Kripke model is a D-model if it is obtained by…
cs.LO2024
Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents
Akinori Maniwa, Ryo Kashima
The cut-elimination procedure for the provability logic is known to be problematic: a Löb-like rule keeps cut-formulae intact on reduction, even in the principal case, thereby com…