直觉主义模态逻辑 S4 的线性逻辑重构
计算机科学中的逻辑
2019-04-25 v1
摘要
我们提出一种“模态线性逻辑”，以线性逻辑重新表述直觉主义模态逻辑 S4（IS4），并建立从 IS4 到该逻辑的 S4 版 Girard 翻译。虽然从直觉主义逻辑到线性逻辑的 Girard 翻译已为人熟知，但其向模态逻辑的扩展并非平凡，因为 S4 模态与指数模态的朴素结合会导致两种模态之间不期望的相互作用。为解决该问题，我们引入直觉主义乘性指数线性逻辑的一个扩展，其带有一个结合 S4 模态与指数模态的模态，并证明它容许从 IS4 的可靠翻译。通过 Curry-Howard 对应，我们进一步由 Pfenning 与 Davies 用于分阶段计算的模态 λ-演算获得了交互几何机（Geometry of Interaction Machine）语义。
引用
@article{arxiv.1904.10605,
title = {A Linear-logical Reconstruction of Intuitionistic Modal Logic S4},
author = {Yosuke Fukuda and Akira Yoshimizu},
journal= {arXiv preprint arXiv:1904.10605},
year = {2019}
}
备注
Author copy of a paper accepted for FSCD 2019