Derivability in certain subsystems of the logic of proofs is \(\Pi_2^p\)-complete
type: Item
instance of: scholarly article
title: Derivability in certain subsystems of the logic of proofs is \(\Pi_2^p\)-complete
zbMATH Open document ID: 1112.03054
published in: Annals of Pure and Applied Logic
publication date: 2007-02-14T00:00:00Z
review text: The Logic of Proofs LP, proposed by S. Artemov, is a realization of the modal logic S4 in which the modality is replaced with explicit terms representing proofs. V. Brezhnev extended the idea of explication to several subsystems, among which the K4 version is of particular interest as the Logic of Beliefs, and R. Kuznets presented a \(\Pi_2^p\) algorithm for deducibility in these logics. In this paper, the author shows that deciding derivability in several significant sybsystems of LP is \(\Pi_2^p\)-hard by encoding QBF-2 as a formula of LP which can be derived only if the quantified Boolean formula is true. From this, in conjuction with the observations by Kuznets, it follows that derivaibility in each of the subsystems is \(\Pi_2^p\)-complete, while the analogous problem for corresponding modal logics is known to be PSPACE-comple.
reviewed by: Osamu Sonobe
Mathematics Subject Classification ID: 03F45
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 68Q17
zbMATH DE Number: 5126406
zbMATH Keywords: logic of proofs
zbMATH Keywords: logic of belief
zbMATH Keywords: complexity
author: Robert Saxon Milnikel
MaRDI profile type: Publication
full work available at URL: j.apal.2006.03.001
OpenAlex ID: W2138312950
cites work: Q4283226
cites work: Explicit provability and constructive semantics
cites work: Q5692429
cites work: Computer Science Logic
cites work: The logic of proofs, semantically
cites work: Q4698331
cites work: Q2753686
cites work: The Computational Complexity of Provability in Systems of Modal Propositional Logic
cites work: Q4376067
cites work: Q3221403
cites work: Q4215637
cites work: Q4716271
DOI: 10.1016/J.APAL.2006.03.001
description: scientific article; zbMATH DE number 5126406