.png){kind=icon}
返回
Interpolation for Converse PDL
.png){kind=icon}
OA
AI
DOI：10.1007/978-3-032-06085-3_14.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
逆PDL是命题动态逻辑在程序上添加逆运算的扩展。我们的主要结果指出，逆PDL在原子程序和命题变量两方面均满足（局部）Craig插值性质。作为推论，我们确立了该逻辑的Beth可定义性性质。我们的插值证明基于对Maehara证明论方法的改进。为此，我们引入了一个适用于该逻辑的可靠且完备的循环sequent系统。该演算具有分析性截取规则，并采用聚焦机制来识别成功的循环。
Keyword:
propositional dynamic logic
converse modalities
cyclic proof system
interpolation
.png){kind=icon}
查看更多内容