|
ИСТИНА |
Войти в систему Регистрация |
ИПМех РАН |
||
On the complexity of explicit modal logicsстатья
- Автор: Kuznets Roman
- Сборник: Computer Science Logic (CSL 2000), 14th Annual Conference of the EACSL, Fischbachau, Germany, August 21-26, 2000, Proceedings
- Серия: Lecture Notes in Computer Science
- Том: 1862
- Год издания: 2000
- Место издания: Springer Berlin
- Первая страница: 371
- Последняя страница: 383
- DOI: 10.1007/3-540-44622-2_25
- Аннотация: Explicit modal logic was introduced by S. Artemov. Whereas the traditional modal logic uses atoms ☐F with a possible semantics “F is provable”, the explicit modal logic deals with atoms of form t:F, where t is a proof polynomial denoting a specific proof of a formula F. Artemov found the explicit modal logic LP in this new format and built an algorithm that recovers explicit proof polynomials corresponding to modalities in every derivation in K. Gödel’s modal provability calculus S4. In this paper we study the complexity of LP as well as the complexity of explicit counterparts of the modal logics K,D,T,KA,D4 found by V. Brezhnev. The main result: the satisfiability problem for each of these explicit modal logics belongs to the class ∑2p 2 of the polynomial hierarchy. Similar problem for the original modal logics is known to be PSPACE-complete. Therefore, explicit modal logics have much better upper complexity bounds than the original modal logics. The author is partially supported by the grant DAAH04-96-1-0341, by DAPRA under program LPE, project 34145.
- Добавил в систему: Золин Евгений Евгеньевич