论文标题
Riesz空间和模态Riesz空间的证明理论
Proof Theory of Riesz Spaces and Modal Riesz Spaces
论文作者
论文摘要
我们为Riesz空间和Modal Riesz空间的理论设计了超平性的演算系统，并证明了关键定理：声音，完整性和剪切消除。然后将这些用于获得有关这两种理论的一些有趣结果的完全句法证明。最值得注意的是，我们证明了一个新的结果：模态Riesz空间的理论是可以决定的。这项工作在概率程序的逻辑领域中具有应用程序，因为Modal Riesz的空间提供了Riesz模态逻辑的代数语义，而概率MU-CALCULUS则是riesz Modal逻辑。
We design hypersequent calculus proof systems for the theories of Riesz spaces and modal Riesz spaces and prove the key theorems: soundness, completeness and cut elimination. These are then used to obtain completely syntactic proofs of some interesting results concerning the two theories. Most notably, we prove a novel result: the theory of modal Riesz spaces is decidable. This work has applications in the field of logics of probabilistic programs since modal Riesz spaces provide the algebraic semantics of the Riesz modal logic underlying the probabilistic mu-calculus.
