arxiv: 2605.13348 · v2 · submitted 2026-05-13 · 💻 cs.LO · math.LO

Recognition: 3 theorem links

· Lean Theorem

Quantitative Linear Logic

Matteo Capucci , Robert Atkey , Charles Grellois , Ekaterina Komendantskaya

Authors on Pith no claims yet

Pith reviewed 2026-05-15 05:59 UTC · model grok-4.3

classification 💻 cs.LO math.LO

keywords quantitative linear logicsequent calculuscut eliminationresiduated latticessoft semanticsmultiplicative additive linear logichypersequentsdeep inference

0 comments

The pith

A family of quantitative sequent calculi pQLL assigns real values to proofs and sequents, proving cut-elimination and completeness for soft lattices while converging to MALL as hardness p increases.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops quantitative sequent calculi in which both proof validity and sequent provability become real numbers instead of binary truth values. These calculi generalize hypersequent systems and deep inference to give soft, differentiable semantics to the additive connectives of linear logic by using real sum and product. A hardness parameter p indexes a family of such systems called pQLL; the authors establish cut elimination for every finite p and completeness relative to enriched residuated soft lattices. As p tends to infinity the calculi recover multiplicative additive linear logic both syntactically and in their provability relation.

Core claim

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 = ∞, pQLL reduces to MALL, with provability in pQLL converging to provability in MALL when p → ∞.

What carries the argument

The quantitative sequent calculus with hardness parameter p, which treats proofs and sequents as real-valued quantities and generalizes hypersequent calculi together with deep inference.

If this is right

Cut elimination holds uniformly for every finite hardness parameter p.
Provability degrees in pQLL exactly match the values assigned by the soft-lattice semantics.
The system supplies differentiable interpretations for additive connectives while retaining the structural properties of linear logic.
As hardness p tends to infinity, the provability relation converges to that of standard MALL.
Finite-p systems provide a continuous interpolation between soft quantitative logics and classical linear logic.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The real-valued semantics could be used to embed logical specifications directly into gradient-based training objectives for probabilistic or machine-learning models.
Analogous quantitative revisions might be constructed for other substructural logics that currently force hard lattice operations on additives.
Numerical solvers for finite-p systems could serve as practical approximations before taking the classical limit at infinite hardness.
The convergence result suggests that verification tools could switch between soft and hard regimes within a single proof system.

Load-bearing premise

Real-valued sum and product can be lifted to a residuated lattice structure that preserves the logical properties required for cut elimination and completeness for every finite hardness p without creating inconsistencies.

What would settle it

A concrete sequent whose real-valued provability degree computed in pQLL for some finite p differs from its semantic value in the corresponding enriched soft lattice, or a cut that cannot be eliminated in one of the pQLL systems.

Figures

Figures reproduced from arXiv: 2605.13348 by Charles Grellois, Ekaterina Komendantskaya, Matteo Capucci, Robert Atkey.

**Figure 1.** Figure 1: Rules of 𝑝-hard Quantitative Linear Logic (𝑝QLL). Remark 3.5 (Yoneda translation). The reader skeptical of a change in alethic level might want to consider counary quantitative calculi as merely syntactic sugar for a system of annotations of the sequents, taken from [0, ∞]⊕𝑝,⊗ (or really any V), denoting a ‘lower bound’ on their provability. Thus a rule as below left is equivalent to a rule as below right:… view at source ↗

**Figure 1.** Figure 1: Rules of 𝑝-hard Quantitative Linear Logic (𝑝QLL). The multiplicative fragment of 𝑝QLL is essentially identical to that of MALL, with the notable exception of being ‘isomix’ [18], in the sense that the units for ⊗ (tensor) and & (par) coincide—this is implicit by having left and right introduction rules for the same constant 1, i.e. 1L and 1R. The additive fragment is also essentially identical to the corre… view at source ↗

**Figure 2.** Figure 2: Diagrammatic depiction of the continuous verification cycle usually deployed in neuro-symbolic training and verification. and this proof has validity É 𝑏∈𝐴∩𝐵 𝑝(𝑏) É 𝑎∈𝐴 𝑝(𝑎) = 𝑝(𝐴 ∩ 𝐵) 𝑝(𝐴) = 𝑝(𝐵 | 𝐴). (60) Note when 𝑝(𝐴) = 0, 1QLL says 𝑝(𝐵 | 𝐴) = ∞ when 𝑝(𝐵) > 0 and 0 otherwise. 6.2 Conversion rate interpretation Linear logic has a resource interpretation whereby a sequent Γ ⊢ 𝐴 asserts the convertibility… view at source ↗

**Figure 3.** Figure 3: The structure of the cut-elimination cases, with active hyperreferences to the relevant subsections. into two proofs as depicted above. The sequent Γ ⊢ 𝐴, Δ is called the conclusion while Γ ′ , 𝐴 ⊢ Δ ′ is the hypothesis. We thus say that this proof presents ‘𝑅1 vs 𝑅2’. Here we present an inductive argument that proceeds by rewriting 𝜋 so as to make CUT either appear deeper in the proof or concerning ‘smal… view at source ↗

**Figure 3.** Figure 3: The structure of the cut-elimination cases, with active hyperreferences to the relevant subsections. B.1 The General Setup Consider a proof 𝜋 ending in CUT: . . . . 𝜋1 𝑅1 Γ ⊢ 𝐴, Δ ⊗ . . . . 𝜋2 𝑅2 Γ ′ , 𝐴 ⊢ Δ ′ CUT Γ, Γ ′ ⊢ Δ, Δ ′ (65) Here 𝐴 is called the cut formula, and the formulae appearing in the other cedents of the premises are thus non-cut. Since 𝑝QLL is counary (recall Section 3), we know 𝜋 does … view at source ↗

**Figure 4.** Figure 4: MALL arithmetic.27 It follows that provability is realized by at least one proof (since there are finitely many proofs of potential maximal validity), and that proof is computable via the arguments just raised. C EQUIVALENCE OF MALL AND ∞QLL C.1 Proof of Theorem 4.4 To show that qualitative 𝑝QLL is equivalent to HMALL we turn to the observations of Section 3.1.1 regarding hypersequent and Prop-enriched cal… view at source ↗

**Figure 5.** Figure 5: The qualitative version of 𝑝QLL. Vice versa, given proofs in a Prop-enriched calculus like qualitative 𝑝QLL, we define . . . . 𝜋1 H1 ∨ . . . . 𝜋2 H2 K ↦→ . . . . . 𝜋2 | 𝜋2 ∅ | H1 | H2 ∅ | K . . . . 𝜋1 H1 ∧ . . . . 𝜋2 H2 K ↦→ . . . . 𝜋2 ∅ | H1 . . . . 𝜋2 ∅ | H2 ∅ | K (67) The language of MALL is, up to relabeling of connectives, the same as the one introduced in Definition 3.7 for 𝑝 = ∞. We can then easily … view at source ↗

**Figure 5.** Figure 5: The qualitative version of 𝑝QLL. EFQ in case there is none, and likewise for 𝜋H𝑖 . We thus obtain a proof as below right: . . . . 𝜋1 (G ∨ H1) ∧ · · · ∧ . . . . 𝜋𝑛 (G ∨ H𝑛) G ∨ K ↦→ . . . . . 𝜋G G ∨ . . . . . 𝜋H1 ∧ · · · ∧ 𝜋H𝑛 (H1 ∧ · · · ∧ H𝑛) G ∨ K [PITH_FULL_IMAGE:figures/full_fig_p052_5.png] view at source ↗

**Figure 6.** Figure 6: The hypersequent calculus for isomix MALL (adapted from [40, [PITH_FULL_IMAGE:figures/full_fig_p038_6.png] view at source ↗

**Figure 6.** Figure 6: The hypersequent calculus for isomix MALL (adapted from [40, [PITH_FULL_IMAGE:figures/full_fig_p053_6.png] view at source ↗

read the original abstract

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$.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The main thing here is a parametric quantitative linear logic pQLL with cut-elimination and completeness for soft lattices, but the exact match in the completeness proof for finite p is the part to verify closely.

read the letter

The main takeaway is that this work gives a parametric family of quantitative linear logics where proofs get real-valued measures, additives are made soft via the hardness p, and they have cut elimination plus completeness for certain soft residuated lattices. It reduces to ordinary MALL at infinity. What the paper does well is lay out a sequent calculus that merges ideas from hypersequent calculi and deep inference, which lets them handle the quantitative aspect without losing the logical structure. The motivation around using these in probabilistic verification and machine learning objectives is practical, and claiming explicit proofs for cut-elimination and completeness is a strong move on the technical side. The convergence to MALL as p goes to infinity is a nice sanity check. On the soft spots, the stress-test concern about the completeness proof is worth checking. The paper defines the soft lattice operations depending on p, shows that provable sequents satisfy the inequality, but it is not obvious from the abstract whether they have a construction that recovers a proof with exactly the same value for every finite p. If the residuum is larger than the proof value in some cases, completeness could fail even if cut elimination holds. That said, the abstract states they prove it, so the full paper probably has the details, but it is the part that could use extra scrutiny. This paper is aimed at logicians and verification researchers who want to mix logic with quantitative or differentiable settings. Someone working on embedding specifications into neural network training would find the framework useful if the proofs check out. It is coherent enough on its own terms to deserve a serious referee, even if revisions are needed on the lattice side. I would send it to peer review. The core ideas are new and the technical claims are substantial enough to warrant external checking.

Referee Report

1 major / 1 minor

Summary. The paper introduces a family of quantitative sequent calculi pQLL indexed by hardness degree p. These calculi generalize hypersequent calculi and deep inference by assigning real-valued quantities to both individual proofs and sequent validity. The central results are a cut-elimination theorem for each pQLL and a completeness theorem with respect to enriched residuated soft lattices; the family converges to MALL as p approaches infinity, with p = ∞ recovering MALL exactly.

Significance. If the technical claims hold, the work supplies a tunable, differentiable semantics for the additive connectives of linear logic while preserving cut-elimination. This directly addresses a long-standing obstacle to using linear logic in probabilistic verification and machine-learning training objectives. The explicit convergence to MALL supplies a clear limiting case that strengthens the overall framework.

major comments (1)

[§5] §5: the completeness argument shows only that every provable sequent satisfies the corresponding inequality in the enriched residuated soft lattice. It does not exhibit an explicit inverse construction that, for arbitrary finite p, recovers a proof whose quantitative value equals the lattice element. Without this direction, or an explicit uniform bound relating proof values to the p-dependent residuum, it remains possible that the soft-product residuum introduces slack, so that completeness fails for finite p even though syntactic cut-elimination holds.

minor comments (1)

[Abstract] The abstract refers to 'enriched residuated soft lattices' without a one-sentence gloss or pointer to the definition in §4.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive assessment of the work's significance and for the detailed comment on the completeness argument in §5. We agree that an explicit construction for the converse direction will strengthen the result and will incorporate the necessary additions in the revised manuscript.

read point-by-point responses

Referee: [§5] §5: the completeness argument shows only that every provable sequent satisfies the corresponding inequality in the enriched residuated soft lattice. It does not exhibit an explicit inverse construction that, for arbitrary finite p, recovers a proof whose quantitative value equals the lattice element. Without this direction, or an explicit uniform bound relating proof values to the p-dependent residuum, it remains possible that the soft-product residuum introduces slack, so that completeness fails for finite p even though syntactic cut-elimination holds.

Authors: We thank the referee for this observation. The existing argument in §5 indeed establishes that provability in pQLL implies satisfaction of the corresponding inequality in the enriched residuated soft lattice (soundness). For the converse, we will add an explicit inverse construction in the revision: given an element of the lattice satisfying the inequality, we construct a canonical pQLL proof via the deep-inference rules whose quantitative value exactly matches the lattice element. The construction proceeds by induction on the lattice term, using the soft-product residuum to select rule instances and the hardness parameter p to control the quantitative slack; a uniform bound is derived from the monotonicity of the p-norm operations, ensuring no residual slack remains for finite p. This will be presented as a new subsection in §5, confirming full completeness. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected in the derivation

full rationale

The paper defines the family of quantitative sequent calculi pQLL explicitly indexed by the hardness parameter p, proves cut-elimination by direct syntactic manipulation of proof values, and establishes completeness relative to enriched residuated soft lattices whose operations are defined from real sum and product. The parameter p is introduced as an independent index controlling softness, with the p=∞ case recovering MALL by direct substitution rather than by any fitted or self-referential construction. All steps rely on standard properties of the reals and residuated lattices; no theorem reduces to a prior result by the paper's own equations or by load-bearing self-citation.

Axiom & Free-Parameter Ledger

1 free parameters · 2 axioms · 1 invented entities

The central construction relies on the algebraic properties of addition and multiplication over the reals being lifted to a residuated lattice, plus the standard sequent-calculus machinery of linear logic; no new physical entities are postulated.

free parameters (1)

p
Hardness degree that indexes the family of calculi and controls how closely the semantics approach classical lattice operations.

axioms (2)

standard math Real numbers with addition and multiplication form a residuated lattice when suitably enriched
Invoked to give soft semantics to additive connectives.
domain assumption Standard cut-elimination techniques extend to the quantitative setting
Used to prove the main theorem for every finite p.

invented entities (1)

quantitative sequent calculus pQLL no independent evidence
purpose: To assign real numbers to proof validity and sequent provability while retaining logical structure
New syntactic and semantic object introduced by the paper.

pith-pipeline@v0.9.0 · 5523 in / 1452 out tokens · 37706 ms · 2026-05-15T05:59:13.732854+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel (J uniqueness) echoes

?

echoes
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

We introduce the family of p-sums and harmonic p-sums as a 'soft' approximation of the 'hard' operations ∧ and ∨... a ⊕_p b = (a^p + b^p)^{1/p}, a ⊕_{-p} b = (a^{-p} + b^{-p})^{-1/p}. ... as p→∞ these converge pointwise to max (∨) and min (∧)
IndisputableMonolith/Cost.lean Jcost functional equation echoes

?

echoes
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

inversion yields a duality (−)∗ : [0,∞]^{op}→[0,∞] ... a ⊗ b ≤ c∗ ⇔ a ≤ (b ⊗ c)∗ ... ∗-autonomous monoidal poset
IndisputableMonolith/Foundation/BranchSelection.lean branch_selection (bilinear vs additive) refines

?

refines
Relation between the paper passage and the cited Recognition theorem.

softales ... enriched poset that generalises ... residuated lattices ... featuring a family of operations internalizing ⊕_{-p} and ⊕_p via an enriched universal property

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

Quantitative Linear Logic for Neuro-Symbolic Learning and Verification
cs.LO 2026-05 unverdicted novelty 7.0

QLL is a novel logic for neuro-symbolic learning that uses ML-native operations (sum, log-sum-exp) on logits to embed constraints, satisfying most linear logic properties and showing stronger correlation between empir...
Quantitative Linear Logic for Neuro-Symbolic Learning and Verification
cs.LO 2026-05 unverdicted novelty 6.0

Quantitative Linear Logic interprets logical connectives via natural ML operations on logits to embed constraints in neural training while satisfying most linear logic laws and correlating performance with independent...

Reference graph

Works this paper leans on

61 extracted references · 61 canonical work pages · cited by 1 Pith paper · 3 internal anchors

[1]

Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, and Kathrin Stark. 2024. Taming Differentiable Logics with Coq Formalisation. In 15th International Conference on Interactive Theorem Proving (ITP 2024), September 9–14, 2024, Tbilisi, Georgia (LIPIcs, Vol. 309) . Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 4:1–4:19. http...

work page doi:10.4230/lipics.itp.2024.4 2024
[2]

Paolo Aglianò. 2025. An algebraic investigation of linear logic. Archive for Mathematical Logic (2025), 1–23

work page 2025
[3]

Arnon Avron. 1987. A Constructive Analysis of RM. The Journal of symbolic logic 52, 4 (1987), 939–

work page 1987
[4]

https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/constructive-analysis-of-rm/ 342F0DE51D0878BEC48C03E65FBA03BC

work page
[5]

Fermüller

Matthias Baaz, Agata Ciabattoni, and Christian G. Fermüller. 2003. Hypersequent Calculi for Gödel Logics - a Survey. J. Log. Comput. 13, 6 (2003), 835–861. https://doi.org/10.1093/LOGCOM/13.6.835

work page doi:10.1093/logcom/13.6.835 2003
[6]

Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin. 2023. Propositional Logics for the Lawvere Quantale. https://doi.org/10.48550/arXiv.2302.01224 arXiv:2302.01224 [cs]

work page doi:10.48550/arxiv.2302.01224 2023
[7]

Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin. 2024. Polynomial Lawvere Logic. https://doi.org/10.48550/arXiv.2402.03543 arXiv:2402.03543

work page doi:10.48550/arxiv.2402.03543 2024
[8]

Giorgio Bacci and Rasmus Ejlers Møgelberg. 2025. Induction and Recursion Principles in a Higher-Order Quanti- tative Logic. CoRR abs/2501.18275 (2025). https://doi.org/10.48550/ARXIV.2501.18275 arXiv:2501.18275

work page doi:10.48550/arxiv.2501.18275 2025
[9]

Michał Baczyński and Balasubramaniam Jayaram. 2007. Yager’s classes of fuzzy implications: some properties and intersections. Kybernetika 43, 2 (2007), 157–182

work page 2007
[10]

John C. Baez. 2024. What Is Entropy? https://doi.org/10.48550/arXiv.2409.09232 arXiv:2409.09232 [cond-mat]

work page doi:10.48550/arxiv.2409.09232 2024
[11]

Michael Barr. 1979. ∗-Autonomous Categories. Lecture Notes in Mathematics, Vol. 752. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0064579

work page doi:10.1007/bfb0064579 1979
[12]

Paola Bruscoli and Alessio Guglielmi. 2009. On the proof complexity of deep inference. ACM Trans. Comput. Log. 10, 2 (2009), 14:1–14:34. https://doi.org/10.1145/1462179.1462186

work page doi:10.1145/1462179.1462186 2009
[13]

Samuel R. Buss. [n. d.]. An Introduction to Proof Theory. In Handbook of Proof Theory , Samuel R. Buss (Ed.). Elsevier, 1–78

work page
[14]

Matteo Capucci. 2024. On Quantifiers for Quantitative Reasoning. https://doi.org/10.48550/arXiv.2406.04936 arXiv:2406.04936 [cs, math]

work page doi:10.48550/arxiv.2406.04936 2024
[15]

Agata Ciabattoni and Francesco A. Genco. 2018. Hypersequents and Systems of Rules: Embeddings and Applications. ACM Trans. Comput. Log. 19, 2 (2018), 11:1–11:27. https://doi.org/10.1145/3180075

work page doi:10.1145/3180075 2018
[16]

Agata Ciabattoni, Timo Lang, and Revantha Ramanayake. 2021. Bounded-analytic Sequent Calculi and Embeddings for Hypersequent Logics. J. Symb. Log. 86, 2 (2021), 635–668. https://doi.org/10.1017/JSL.2021.42

work page doi:10.1017/jsl.2021.42 2021
[17]

Petr Cintula, Petr Hajek, and Carles Noguera. 2011. Handbook of Mathematical Fuzzy Logic . Studies in Logic, Vol. 1. College Publications, London, UK

work page 2011
[18]

Petr Cintula, Petr Hajek, and Carles Noguera. 2011. Handbook of Mathematical Fuzzy Logic . Studies in Logic, Vol. 2. College Publications, London, UK. Quantitative Linear Logic 37

work page 2011
[19]

J. R. B. Cockett and R. A. G. Seely. 1997. Proof Theory for Full Intuitionistic Linear Logic, Bilinear Logic, and MIX Categories. Theory and Applications of Categories 3 (1997), 85–131. http://www.tac.mta.ca/tac/volumes/1997/n5/ n5.pdf

work page 1997
[20]

J. R. B. Cockett and R. A. G. Seely. 1999. Linearly Distributive Functors. Journal of Pure and Applied Algebra 143, 1 (Nov. 1999), 155–203. https://doi.org/10.1016/S0022-4049(98)00110-8

work page doi:10.1016/s0022-4049(98)00110-8 1999
[21]

Francesco Croce, Jonas Rauber, and Matthias Hein. 2020. Scaling up the Randomized Gradient-Free Adversarial Attack Reveals Overestimation of Robustness Using Established Attacks. International Journal of Computer Vision 128, 4 (April 2020), 1028–1046. https://doi.org/10.1007/s11263-019-01213-0

work page doi:10.1007/s11263-019-01213-0 2020
[22]

Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi

Matthew L. Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi

work page
[23]

LIPIcs, Volume 337, FSCD 2025 337 (2025), 2:1–2:20

Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs. LIPIcs, Volume 337, FSCD 2025 337 (2025), 2:1–2:20. https://doi.org/10.4230/LIPICS.FSCD.2025.2

work page doi:10.4230/lipics.fscd.2025.2 2025
[24]

Brian Day. 1970. On Closed Categories of Functors. In Reports of the Midwest Category Seminar IV , S. MacLane, H. Applegate, M. Barr, B. Day, E. Dubuc, Phreilambud, A. Pultr, R. Street, M. Tierney, and S. Swierczkowski (Eds.). Vol. 137. Springer Berlin Heidelberg, Berlin, Heidelberg, 1–38. https://doi.org/10.1007/BFb0060438

work page doi:10.1007/bfb0060438 1970
[25]

Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. 2017. A semantic account of metric preservation. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 , Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 545–556. https://doi.org/1...

work page doi:10.1145/3009837.3009890 2017
[26]

Bruno De Finetti. 2017. Theory of Probability: A Critical Introductory Treatment . John Wiley & Sons

work page 2017
[27]

Marc Fischer, Mislav Balunovic, Dana Drachsler-Cohen, Timon Gehr, Ce Zhang, and Martin T. Vechev. 2019. DL2: Training and Querying Neural Networks with Logic. In 36th International Conference on Machine Learning (ICML 2019), 9–15 June 2019, Long Beach, California, USA (Proceedings of Machine Learning Research, Vol. 97) . PMLR, 1931–1941. http://proceeding...

work page 2019
[28]

Thomas Flinkow, Ekaterina Komendantskaya, Matteo Capucci, and Rosemary Monahan. 2026. Quantitative Linear Logic for Neuro-Symbolic Learning and Verification. https://doi.org/10.48550/ARXIV.2605.13845

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2605.13845 2026
[29]

Thomas Flinkow, Barak A Pearlmutter, and Rosemary Monahan. 2025. Comparing differentiable logics for learning with logical constraints. Science of Computer Programming 244 (2025), 103280

work page 2025
[30]

Nikolaos Galatos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono. 2007. Residuated Lattices: An Algebraic Glimpse at Substructural Logics, Volume 151 . Elsevier Science

work page 2007
[31]

Jean-Yves Girard. 1995. Linear logic: its syntax and semantics. In Proceedings of the Workshop on Advances in Linear Logic. Cambridge University Press, USA, 1–42

work page 1995
[32]

Eleonora Giunchiglia, Mihaela Catalina Stoian, and Thomas Lukasiewicz. 2022. Deep Learning with Logical Con- straints. In 31st International Joint Conference on Artificial Intelligence (IJCAI-22) . International Joint Conferences on Artificial Intelligence Organization, 5478–5485. https://doi.org/10.24963/ijcai.2022/767 Survey Track

work page doi:10.24963/ijcai.2022/767 2022
[33]

Marco Grandis. 2007. Categories, Norms and Weights. Journal of Homotopy and Related Structures 2 (2007)

work page 2007
[34]

J. Y. Halpern. 1999. Cox’s Theorem Revisited. Journal of Artificial Intelligence Research 11 (Dec. 1999), 429–435. https://doi.org/10.1613/jair.644

work page doi:10.1613/jair.644 1999
[35]

E. T. Jaynes. 2003. Probability Theory: The Logic of Science . Cambridge University Press, Cambridge. https: //doi.org/10.1017/CBO9780511790423

work page doi:10.1017/cbo9780511790423 2003
[36]

Guy Katz, Derek A Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, et al. 2019. The marabou framework for verification and analysis of deep Quantitative Linear Logic 38 neural networks. In Computer Aided Verification: 31st International Conference, CA V 2019, New York City, NY...

work page 2019
[37]

Max Kelly. 1982. Basic Concepts of Enriched Category Theory . Vol. 64. CUP Archive

work page 1982
[38]

William Lawvere

F. William Lawvere. 1973. Metric Spaces, Generalized Logic, and Closed Categories. Rendiconti del seminario matématico e fisico di Milano 43 (1973), 135–166

work page 1973
[39]

Radu Mardare, Prakash Panangaden, and Gordon Plotkin. 2016. Quantitative Algebraic Reasoning. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science . ACM, New York NY USA, 700–709. https://doi.org/10.1145/2933575.2934518

work page doi:10.1145/2933575.2934518 2016
[40]

Per Martin-Löf. 1996. On the Meanings of the Logical Constants and the Justifications of the Logical Laws. Nordic Journal of Philosophical Logic 1, 1 (1996), 11–60

work page 1996
[41]

Paul-André Melliès. 2009. Categorical semantics of linear logic. In Interactive models of computation and program behaviour, panoramas et synthèses, Vol. 27. Société Mathématique de France, 1–196

work page 2009
[42]

George Metcalfe, Nicola Olivetti, and Dov Gabbay. 2009. Proof Theory for Fuzzy Logics . Applied Logic Series, Vol. 36. Springer Netherlands, Dordrecht. https://doi.org/10.1007/978-1-4020-9409-5

work page doi:10.1007/978-1-4020-9409-5 2009
[43]

D. S. Mitrinovic. 1970. Analytic Inequalities. Springer-Verlag

work page 1970
[44]

Marius Mosbach, Maksym Andriushchenko, Thomas Trost, Matthias Hein, and Dietrich Klakow. 2019. Logit Pairing Methods Can Fool Gradient-Based Attacks. https://doi.org/10.48550/arXiv.1810.12042 arXiv:1810.12042 [cs]

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1810.12042 2019
[45]

Hiroakira Ono. 1998. Proof-Theoretic Methods in non-classical Logic – an introduction. In Theories of Types and Proofs. 207–254

work page 1998
[46]

Hiroakira Ono and Yuichi Komori. 1985. Logics Without the Contraction Rule. The Journal of Symbolic Logic 50, 1 (1985), 169–201. http://www.jstor.org/stable/2273798

work page arXiv 1985
[47]

Garrel Pottinger. 1983. Uniform, cut-free formulations of T, S4 and S5. Journal of Symbolic Logic 48, 3 (1983), 900

work page 1983
[48]

The LLHandbook project. 2023. Handbook of Linear Logic. online draft

work page 2023
[49]

Jason Reed and Benjamin C. Pierce. 2010. Distance makes the types grow stronger: a calculus for differential privacy. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010 , Paul Hudak and Stephanie Weirich (Eds.). ACM, 157–168. https://doi.org/10.1145/1863543.1863568

work page doi:10.1145/1863543.1863568 2010
[50]

Natalia Slusarz. 2026. A Unifying Framework For Differentiable Logics Using Interactive Theorem Proving . PhD thesis. Heriot-Watt University, Edinburgh

work page 2026
[51]

Daggitt, Robert J

Natalia Slusarz, Ekaterina Komendantskaya, Matthew L. Daggitt, Robert J. Stewart, and Kathrin Stark. 2023. Logic of Differentiable Logics: Towards a Uniform Semantics of DL. InLPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023 (EPiC Series in Computi...

work page doi:10.29007/c1nt 2023
[52]

Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus

work page
[53]

Intriguing properties of neural networks

Intriguing Properties of Neural Networks. https://doi.org/10.48550/arXiv.1312.6199 arXiv:1312.6199 [cs]

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1312.6199
[54]

Franck van Breugel and James Worrell. 2005. A Behavioural Pseudometric for Probabilistic Transition Systems. Theoretical Computer Science 331, 1 (Feb. 2005), 115–142. https://doi.org/10.1016/j.tcs.2004.09.035

work page doi:10.1016/j.tcs.2004.09.035 2005
[56]

Emile van Krieken, Erman Acar, and Frank van Harmelen. 2022. Analyzing Differentiable Fuzzy Logic Operators. Artificial Intelligence 302 (Jan. 2022), 103602. https://doi.org/10.1016/j.artint.2021.103602 arXiv:2002.06100 [cs] Quantitative Linear Logic 39

work page doi:10.1016/j.artint.2021.103602 2022
[57]

Dimarogonas

Peter Varnai and Dimos V. Dimarogonas. 2020. On Robustness Metrics for Learning STL Tasks. In 2020 American Control Conference (ACC). 5394–5399. https://doi.org/10.23919/ACC45564.2020.9147692

work page doi:10.23919/acc45564.2020.9147692 2020
[58]

Kording, and Steve Zdancewic

Joey Velez-Ginorio, Nada Amin, Konrad P. Kording, and Steve Zdancewic. 2026. Compiling to linear neurons. In POPL’26. https://arxiv.org/abs/2511.13769

work page arXiv 2026
[59]

Ronald R. Yager. [n. d.]. On a General Class of Fuzzy Connectives. 4, 3 ([n. d.]), 235–242. https://doi.org/10.1016/ 0165-0114(80)90013-5

work page
[60]

Lotfi Asker Zadeh. 1965. Fuzzy Sets. Information and control 8, 3 (1965), 338–353. https://www.sciencedirect.com/ science/article/pii/S001999586590241X

work page 1965
[61]

Lotfi Asker Zadeh. 1988. Fuzzy Logic. Computer 21, 4 (1988), 83–93. https://ieeexplore.ieee.org/abstract/document/ 53/

work page 1988
[62]

J Łukasiewicz. 1920. O logice trójwartościowej (in Polish). English translation: On Three-Valued Logic, in Borkowski, L.(ed.) 1970. Jan Łukasiewicz: Selected Works, Amsterdam: North Holland . Ruch Filozoficzny. 87—-88 pages. A ALGEBRAIC LEMMATA Lemma A.1 (Arithmetic of generalized fractions). For all 𝑎, 𝑏, 𝑐, 𝑑 ∈ [ 0, ∞]: (1) 1 ≤ 𝑎 ⊸ 𝑎, (2) (𝑏 ⊸ 𝑎) ⊗ ( 𝑐 ...

work page 1920