On the unification problem for GLP
arxiv(2024)
摘要
We show that the polymodal provability logic GLP, in a language with at least
two modalities and one variable, has nullary unification type. More
specifically, we show that the formula [1]p does not have maximal unifiers, and
exhibit an infinite complete set of unifiers for it. Further, we discuss the
algorithmic problem of whether a given formula is unifiable in GLP and remark
that this problem has a positive solution. Finally, we state the arithmetical
analogues of the unification and admissibility problems for GLP and formulate a
number of open questions.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要