Sabotage modal logic (SML) is a kind of dynamic logics. It extends static modal logic with a dynamic modality which is interpreted as "after deleting an arrow in the frame, the formula is true". In the present paper, we are aiming at solving an open problem, namely giving a Sahlqvist-type correspondence theorem for sabotage modal logic. In this paper, we define sabotage Sahlqvist formulas and give an algorithm to compute the first-order correspondents of sabotage Sahlqvist formulas. We give some remarks and future directions at the end of the paper.
翻译:破坏模式逻辑(SML)是一种动态逻辑(SML),它以动态模式扩展静态模式逻辑,其动态模式被解释为“在删除框架中的箭后,公式是真实的”。 在本文中,我们的目标是解决一个尚未解决的问题,即给Sahlqvist型通信模式逻辑提供破坏模式逻辑的理论。在本文中,我们定义了破坏Sahlqvist公式,并给出了计算破坏Sahlqvist公式的第一阶记者的算法。我们在论文结尾处给出了一些评论和未来方向。