论文标题
松弛逻辑的证明理论
Proof Theory for Lax Logic
论文作者
论文摘要
在本文中，开发了一些有关命题松弛逻辑的证明理论。为逻辑引入了一个切割的自由终止序列演算，并基于该积分表明逻辑具有统一的插值。此外，还提供了一个单独的简单插值证明，它也使用了序列的演算。从文献来看，众所周知，松弛逻辑具有插值，但是所有已知的证明都使用模型而不是证明系统。
In this paper some proof theory for propositional Lax Logic is developed. A cut free terminating sequent calculus is introduced for the logic, and based on that calculus it is shown that the logic has uniform interpolation. Furthermore, a separate, simple proof of interpolation is provided that also uses the sequent calculus. From the literature it is known that Lax Logic has interpolation, but all known proofs use models rather than proof systems.
