首页/论文/2004.06398

arXiv 2004.063982020-04-14math.LO

The closed fragment of IL is PSPACE hard

Félix Bou, Joost J. Joosten

发表信息：: Elsevier, Electronic Notes in Theoretical Computer Science, Volume 278 (47-54), 2011

英文摘要：

In this paper from 2011 we consider $\textbf{IL}_0$, the closed fragment of the basic interpretability logic $\textbf{IL}$. We show that we can translate $\textbf{GL}_1$, the one variable fragment of Gödel-Löb's provabilty logic $\textbf{GL}$, into $\textbf{IL}_0$. Invoking a result on the PSPACE completeness of $\textbf{GL}_1$ we obtain the PSPACE hardness of $\textbf{IL}_0$.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

仅基于垂直关系的初等平面欧几里得几何片段及其PSPACE完全复杂性

The fragment of elementary plane Euclidean geometry based on perpendicularity alone with complexity PSPACE-complete

本文对仅以垂直关系为原始关系的初等平面欧几里得几何片段给出完整公理化，证明该理论不可有限公理化、可判定且复杂性为PSPACE完全，区别于完整初等平面几何的指数级复杂性。

2021-07-21math.LO

Complexity of the variable-free fragment of the weak Grzegorczyk logic

The paper proves PSPACE-hardness of variable-free fragments of all logics between K and wGrz.

2022-11-26math.LO

Complexity of the interpretability logic IL

We show that the decision problem for the basic system of interpretability logic IL is PSPACE-complete. For this purpose we present an algorithm which uses polynomial space with respect to the complexity of a given formula. The existence of such algorithm, together with the previously known PSPACE hardness of the closed fragment of IL, implies PSPACE-completeness.

2018-04-06math.LO

具有收敛公理的逻辑：语言中变量数量较少时的复杂性（扩展版）

Logics with the axiom of convergence: complexity with a small number of variables in the language (extended version)

本文研究了添加收敛公理的模态逻辑S4.2、K4.2、Grz.2和GL.2在少变量语言中的复杂性，证明S4.2和Grz.2在双变量语言中为PSPACE完全，K4.2和GL.2*在单变量语言中为PSPACE完全，并将结果推广到无穷逻辑类。

2025-09-24math.LO

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

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

2013-05-26math.LO

Generalized Hex and logical characterizations of polynomial space

We answer a question posed by Makowsky and Pnueli and show that the logic $(\pm\mbox{HEX})^\ast[\mbox{FO}_s]$, where HEX is the operator (i.e., uniform sequence of Lindström quantifiers) corresponding to the well-known {\bf PSPACE}-complete decision problem Generalized Hex, collapses to the fragment $\mbox{HEX}^1[\mbox{FO}_s]$ and, moreover, that this logic has a particular normal form which results in the problem HEX being complete for {\bf PSPACE} via quantifier-free projections with successor (HEX is the first ``natural'' problem to be shown to have this property). Our proof of this normal …

1996-12-01math.LO

更多相关论文收起更多论文

Complexity of finite-variable fragments of propositional modal logics of symmetric frames

While finite-variable fragments of the propositional modal logic S5--complete with respect to reflexive, symmetric and transitive frames--are polynomial-time decidable, the restriction to finite-variable formulas for logics of reflexive and transitive frames yields fragments that remain "intractable." The role of the symmetry condition in this context has not been investigated. We show that symmetry either by itself or in combination with reflexivity produces logics that behave just like logics of reflexive and transitive frames, i.e. their finite-variable fragments remain intractable, namely …

2019-10-05cs.LOmath.LO

Bundled fragments of first-order modal logic: (un)decidability

Institute of Mathematical Sciences, Homi Bhabha National Institute（数学科学研究所，霍米·巴巴国家研究所）；Peking University（北京大学）

Quantified modal logic provides a natural logical language for reasoning about modal attitudes even while retaining the richness of quantification for referring to predicates over domains. But then most fragments of the logic are undecidable, over many model classes. Over the years, only a few fragments (such as the monodic) have been shown to be decidable. In this paper, we study fragments that bundle quantifiers and modalities together, inspired by earlier work on epistemic logics of know-how/why/what. As always with quantified modal logics, it makes a significant difference whether the doma…

2018-03-28cs.AIcs.LOmath.LO

EXPSPACE-Completeness of the Logics K4xS5 and S4xS5 and the Logic of Subset Spaces, Part 2: EXPSPACE-Hardness

It is known that the satisfiability problems of the product logics K4xS5 and S4xS5 are NEXPTIME-hard and that the satisfiability problem of the logic SSL of subset spaces is PSPACE-hard. We improve these lower bounds for the complexity of these problems by showing that all three problems are EXPSPACE-hard under logspace reduction. In another paper we show that these problems are in ESPACE. This shows that all three problems are EXPSPACE-complete.

2019-08-09cs.CCcs.LOmath.LO

Rules with parameters in modal logic II

We analyze the computational complexity of admissibility and unifiability with parameters in transitive modal logics. The class of cluster-extensible (clx) logics was introduced in the first part of this series of papers. We completely classify the complexity of unifiability or inadmissibility in any clx logic as being complete for one of $Σ^{\exp}_2$, NEXP, coNEXP, PSPACE, or $Π^p_2$. In addition to the main case where arbitrary parameters are allowed, we consider restricted problems with the number of parameters bounded by a constant, and the parameter-free case. Our upper bounds are specifi…

2020-05-03cs.LOmath.LO

通过线性化优化 Gödel-Löb 逻辑的树-超矢列证明搜索

Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents

TU Dresden（德累斯顿工业大学）

针对 GL 逻辑在树-超矢列系统 CSGL 中的可判定性证明和 PSPACE 证明搜索算法问题，提出线性化方法，仅构建单分支推导和树矢列，实现 PSPACE 最优复杂度，并提取有限反模型验证算法正确性。

2026-08-11cs.LOmath.LO