Real-valued logics have seen a renewed interest in verification for probabilistic and quantitative systems, in particular machine learning models, where they can be used to directly integrate specifications in the training objective. To do so effectively one has to strike a balance between the logical properties of the connectives and their semantics. A major hurdle in this sense is to give ``soft'' (i.e. differentiable) semantics to additive connectives -- in linear and fuzzy logics, additives are necessarily ``hard'' lattice operations. In this paper, we solve this problem by combining an accurate analysis of the properties of sum and product on the reals with a significant revision of sequent calculus. We introduce `quantitative sequent calculi', which simultaneously generalize hypersequent calculi of fuzzy logics and deep inference, and in which validity of a proof and provability of a sequent are real-valued quantities. We present a family of calculi, pQLL, indexed by a hardness degree $p$, prove cut-elimination theorem for them, and show completeness for enriched residuated `soft' lattices. For $p = \infty$, pQLL reduces to MALL, with provability in pQLL converging to provability in MALL when $p \to \infty$.

翻译：实值逻辑在概率与量化系统（尤其是机器学习模型）的验证中重新受到关注，此类逻辑可直接将规范整合到训练目标中。要有效实现这一目标，需在联结词的逻辑性质与其语义之间取得平衡。主要障碍在于为加性联结词赋予“软”（即可微）语义——在线性逻辑与模糊逻辑中，加性联结词必然是“硬”的格运算。本文通过结合实数上加法与乘法性质的精确分析，并对矢列演算进行重要修正，解决了该问题。我们提出“定量矢列演算”，该演算同时推广了模糊逻辑的超矢列演算与深度推理，其中证明的有效性与矢列的可证性均为实数值量。我们展示了由硬度参数$p$索引的演算族pQLL，证明了其切割消去定理，并给出了富化剩余“软”格的完备性。当$p = \infty$时，pQLL退化为MALL，且当$p \to \infty$时pQLL中的可证性收敛至MALL中的可证性。