What is it about?
One of the fundamental complexity-theoretic results about logic is the theorem by Cook and Levin, which says that the satisfiability problem for Boolean formulas is NP-complete. Since then the complexity of problems in many other logics has been analyzed. In this article, we are concerned with the complexity of the bimodal product logics K4 × S5 and S4 × S5 and with the subset space logic SSL, a bimodal logic as well. The main results of this article are summarized in the following theorem. Theorem. The logics K4 × S5, S4 × S5, and SSL are in ESPACE and are EXPSPACE-complete under logspace reduction.
Featured Image
Why is it important?
It is known that the satisfiability problems of the product logics K4 × S5 and S4 × S5 are NEXPTIME-hard and that the satisfiability problem of the logic SSL of subset spaces is PSPACE-hard. Furthermore, it is known that the satisfiability problems of these logics are in N2EXPTIME. We improve the lower and the upper bounds for the complexity of these problems by showing that all three problems are in ESPACE and are EXPSPACEcomplete under logspace reduction.
Perspectives
Important aspects of the proof of the EXPSPACE-hardness of the logic SSL of subset spaces were the following: 1. The development of certain formulas that enabled us to overcome the problem that in SSL the usual propositional variables are persistent. 2. The use of alternating Turing machines. Although they are kwown for decades and have been used for establishing lower bounds for the complexity of certain logics, they seem to not that common in modal logic.
Peter Hertling
Universitat der Bundeswehr Munchen
Read the Original
This page is a summary of: EXPSPACE-Completeness of the Logics K4 × S5 and S4 × S5 and the Logic of Subset Spaces, ACM Transactions on Computational Logic, October 2021, ACM (Association for Computing Machinery),
DOI: 10.1145/3465384.
You can read the full text:
Contributors
The following have contributed to this page
