Derivability in certain subsystems of the logic of proofs is \(\Pi_2^p\)-complete (Q866565)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Derivability in certain subsystems of the logic of proofs is \(\Pi_2^p\)-complete |
scientific article |
Statements
Derivability in certain subsystems of the logic of proofs is \(\Pi_2^p\)-complete (English)
0 references
14 February 2007
0 references
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.
0 references
logic of proofs
0 references
logic of belief
0 references
complexity
0 references