On the complexity of the closed fragment of Japaridze's provability logic

Abstract

We consider well-known provability logic GLP. We prove that the GLP-provability problem for variable-free polymodal formulas is PSPACE-complete. For a number n, let L^n_0 denote the class of all polymodal variable-free formulas without modalities <n>, <n+1>,... . We show that, for every number n, the GLP-provability problem for formulas from L^n_0 is in PTIME.

arXiv comment12 pages, the results of this work and a proof sketch are in Advances in Modal Logic 2012 extended abstract on the same name

Cited by in corpus (1)

• On provability logics with linearly ordered modalities