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

2013/05/26 by Fedor Pakhomov, Pakhomov, Fedor
Computer Science · #03F45 #F.2.2 #F.4.1 #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies

paper · pdf · doi:10.48550/arxiv.1305.6065

openalex publication_date 2013/05/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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ⁿ₀ denote the class of all polymodal variable-free formulas without modalities , ,... . We show that, for every number n, the GLP-provability problem for formulas from Lⁿ₀ is in PTIME.

Related

• On provability logics with linearly ordered modalities
• On the unification problem for GLP
• Logics with the axiom of convergence: complexity with a small number of variables in the language (extended version)
• On Elementary Theories of GLP-Algebras
• On Logic of Formal Provability and Explicit Proofs