paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Proof Theory of Riesz Spaces and Modal Riesz Spaces

Riesz 空间与模态 Riesz 空间的证明论
LMCS vol.Volume 18, Issue 12022匹配度 3/10 · 论文属于概率程序逻辑与证明论，与形式化验证有间接关联，但不涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析，与用户当前研究画像的核心方向匹配度较低。引用 1 inbox
Christophe Lucas, Matteo Mio
定理证明与证明工程逻辑与自动机
crossref: 2026-09-10

AI 速览

一句话：为 Riesz 空间与模态 Riesz 空间设计超序列演算，证明可靠、完备与切消，并据此给出模态 Riesz 空间可判定性的新证明。

本文研究 Riesz 空间与模态 Riesz 空间的证明论。Riesz 空间与模态 Riesz 空间分别为概率程序逻辑中的 Riesz 模态逻辑及概率 μ-演算提供代数语义，但其证明系统此前尚不完整。作者为这两个理论设计超序列演算（hypersequent calculus），并证明可靠性、完备性与切消定理。借助这些证明论结果，他们给出若干关于两个理论的完全语法化证明，其中最值得注意的是证明了模态 Riesz 空间理论的可判定性。该工作将证明论方法引入概率程序逻辑的代数语义，为概率 μ-演算的推理与判定提供了新工具。

问题
为 Riesz 空间与模态 Riesz 空间建立证明系统，并解决其可靠性、完备性、切消等证明论性质以及模态 Riesz 空间的可判定性问题。
方法
设计超序列演算（hypersequent calculus）作为 Riesz 空间与模态 Riesz 空间理论的证明系统，并证明 soundness、completeness 与 cut elimination。
评估
通过证明论定理给出两个理论的完全语法化证明；关键评估结果是证明模态 Riesz 空间理论可判定，并联系到概率 μ-演算的代数语义。
原文摘要（Abstract）

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.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@article{paperbot1723,
  title = {Proof Theory of Riesz Spaces and Modal Riesz Spaces},
  author = {Christophe Lucas and Matteo Mio},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 1},
  year = {2022},
  doi = {10.46298/lmcs-18(1:32)2022}
}