pith. machine review for the scientific record. sign in

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

Recognition: no theorem link

Quantitative Linear Logic

Charles Grellois, Ekaterina Komendantskaya, Matteo Capucci, Robert Atkey

Authors on Pith no claims yet

Pith reviewed 2026-05-14 18:50 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords quantitative sequent calculuslinear logicsoft semanticscut-eliminationresiduated latticesfuzzy logicdeep inferencereal-valued provability
0
0 comments X

The pith

Quantitative sequent calculi assign real-valued measures to proofs and sequents in linear logic.

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

The paper introduces a family of quantitative sequent calculi called pQLL that generalize hypersequent systems and deep inference. In these calculi, the validity of a proof and the provability of a sequent become real numbers instead of binary outcomes. This change is achieved by revising the rules of sequent calculus to incorporate the algebraic properties of sum and product on the reals, which softens the additive connectives while keeping their logical behavior intact. The authors prove that cut-elimination holds for every member of the family and that the systems are complete with respect to enriched residuated soft lattices. As the hardness parameter p tends to infinity, pQLL recovers ordinary multiplicative-additive linear logic.

Core claim

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

What carries the argument

The pQLL family of quantitative sequent calculi, indexed by hardness degree p, which revises sequent rules so that proof validity and sequent provability become real-valued quantities computed from sums and products.

If this is right

  • Cut-elimination holds uniformly for the entire parameterized family pQLL.
  • Completeness is obtained with respect to enriched residuated soft lattices.
  • Provability measures converge to those of standard MALL in the limit as p tends to infinity.
  • Additive connectives receive soft, real-valued semantics that remain compatible with the multiplicative fragment.

Where Pith is reading between the lines

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

  • The real-valued provability could be inserted directly as a differentiable term inside gradient-based optimization loops for systems that must satisfy logical specifications.
  • Similar quantitative revisions might be applied to other proof systems to produce graded notions of validity for uncertain or probabilistic reasoning tasks.
  • The hardness parameter p offers a tunable knob that interpolates between fully soft and fully crisp logical behavior.

Load-bearing premise

That an accurate analysis of sum and product on the reals, combined with a quantitative revision of sequent rules, can preserve the logical properties of additives while making their semantics soft and differentiable.

What would settle it

A concrete sequent whose provability measure in pQLL fails to approach 1 as p grows without bound, or a cut that cannot be eliminated for some finite value of p.

Figures

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

Figure 1
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 2
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. Figure 3: The structure of the cut-elimination cases, with active hyperreferences to the relevant subsec￾tions. 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 4
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. 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 6
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 ↗
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.

Referee Report

2 major / 2 minor

Summary. The paper introduces quantitative sequent calculi (pQLL), a family indexed by hardness degree p, that generalize hypersequent calculi of fuzzy logics and deep inference. In these calculi, both proof validity and sequent provability are real-valued quantities obtained via sum and product operations on the reals. The authors prove cut-elimination for pQLL and completeness with respect to enriched residuated soft lattices; the p → ∞ limit recovers standard MALL.

Significance. If the cut-elimination and completeness results hold, the work provides a technically novel route to soft, differentiable semantics for additive connectives while retaining residuation and cut-elimination. This directly addresses a central obstacle in applying real-valued logics to probabilistic verification and machine-learning training objectives. The algebraic analysis of sum/product and the uniform p-parameterization that interpolates between soft and hard behavior are genuine strengths.

major comments (2)
  1. [Cut-elimination proof] The cut-elimination argument (stated in the abstract and presumably detailed after the definition of pQLL rules) must explicitly track how the real-valued measure is preserved or decreased under each reduction step; without this, it is unclear whether the quantitative interpretation remains compatible with the standard logical properties of additives.
  2. [Completeness theorem] Completeness for enriched residuated soft lattices (abstract and main completeness theorem) depends on the precise definition of the soft lattice operations and the enrichment; the manuscript should supply an explicit verification that the quantitative provability measure coincides with the lattice order without additional ad-hoc parameters beyond p.
minor comments (2)
  1. [Abstract] Notation for the real-valued validity measure should be introduced once and used consistently; currently the abstract mixes 'validity of a proof' and 'provability of a sequent' without a single symbol.
  2. [Introduction] The statement that pQLL 'simultaneously generalizes hypersequent calculi and deep inference' would benefit from a short comparative table or paragraph locating the new rules relative to existing hypersequent and deep-inference presentations.

Circularity Check

0 steps flagged

No significant circularity in derivation of quantitative sequent calculi

full rationale

The paper defines quantitative sequent calculi as a novel generalization of hypersequent calculi and deep inference, then independently proves cut-elimination for the pQLL family and completeness relative to enriched residuated soft lattices. The real-valued provability measure is introduced as part of this construction rather than fitted from data or reduced by definition to prior results. The p to infinity limit recovering MALL is presented as a convergence theorem, not a tautological equivalence. No load-bearing step relies on self-citation chains or renames known patterns; the algebraic analysis of sum/product enables the soft semantics while preserving residuation, keeping the central claims self-contained.

Axiom & Free-Parameter Ledger

1 free parameters · 1 axioms · 1 invented entities

The central claim rests on the algebraic properties of real sum and product plus a non-standard revision of sequent calculus; the hardness parameter p is introduced to index the family but is not fitted to data.

free parameters (1)
  • hardness degree p
    Parameter indexing the family pQLL that controls the softness of the semantics; no specific fitted value is given.
axioms (1)
  • domain assumption Properties of sum and product on the reals allow soft semantics for additive connectives
    Invoked to overcome the hardness of lattice operations in linear and fuzzy logics.
invented entities (1)
  • quantitative sequent calculi no independent evidence
    purpose: To assign real-valued validity to proofs and provability to sequents
    New syntactic and semantic object introduced to generalize hypersequents and deep inference.

pith-pipeline@v0.9.0 · 5523 in / 1469 out tokens · 40093 ms · 2026-05-14T18:50:16.070465+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

61 extracted references · 30 canonical work pages · 2 internal anchors

  1. [1]

    Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, and Kathrin Stark. 2024. Taming Differentiable Logics with Coq Formalisation. In15th 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. doi:1...

    work page doi:10.4230/lipics.itp.2024.4 2024

  2. [2]

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

    2025

  3. [3]

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

    1987

  4. [4]

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

  5. [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. doi:10.1093/LOGCOM/13.6.835

    work page doi:10.1093/logcom/13.6.835 2003

  6. [6]

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

    work page doi:10.48550/arxiv.2302.01224 2023

  7. [7]

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

    work page arXiv 2024

  8. [8]

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

    work page doi:10.48550/arxiv.2501.18275 2025

  9. [9]

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

    2007

  10. [10]

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

    work page doi:10.48550/arxiv.2409.09232 2024

  11. [11]

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

    work page doi:10.1007/bfb0064579 1979

  12. [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. doi:10.1145/1462179.1462186

    work page doi:10.1145/1462179.1462186 2009

  13. [13]

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

    1998

  14. [14]

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

    work page doi:10.48550/arxiv.2406.04936 2024

  15. [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. doi:10.1145/3180075

    work page doi:10.1145/3180075 2018

  16. [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. doi:10.1017/JSL.2021.42

    work page doi:10.1017/jsl.2021.42 2021

  17. [17]

    Petr Cintula, Petr Hajek, and Carles Noguera. 2011. Handbook of Mathematical Fuzzy Logic . Studies in Logic, Vol. 1. College Publications, London, UK. Proc. ACM Program. Lang., Vol. 0, No. POPL, Article 0. Publication date: May 2027. 0:26 Capucci et al

    2011

  18. [18]

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

    2011

  19. [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

    1997

  20. [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. doi:10.1016/S0022-4049(98)00110-8

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

  21. [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. doi:10.1007/s11263-019-01213-0

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

  22. [22]

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

    Matthew L. Daggitt, Wen Kokke, Robert Atkey, Natalia Ślusarz, Luca Arnaboldi, and Ekaterina Komendantskaya. 2025. Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs. InProceedings of FSCD’2025. arXiv:2401.06379 [cs.AI]

    work page arXiv 2025

  23. [23]

    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. doi:10.1007/BFb0060438

    work page doi:10.1007/bfb0060438 1970

  24. [24]

    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. doi:10.1145/30098...

    work page doi:10.1145/3009837.3009890 2017

  25. [25]

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

    2017

  26. [26]

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

    2019

  27. [27]

    Thomas Flinkow, Ekaterina Komendantskaya, Matteo Capucci, and Rosemary Monahan. 2026. Quantitative Linear Logic for Neuro-Symbolic Learning and Verification. (2026). Forthcoming preprint

    2026

  28. [28]

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

    2025

  29. [29]

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

    2007

  30. [30]

    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

    1995

  31. [31]

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

    work page doi:10.24963/ijcai.2022/767 2022

  32. [32]

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

    2007

  33. [33]

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

    work page doi:10.1613/jair.644 1999

  34. [34]

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

    2003

  35. [35]

    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 neural networks. In Computer Aided Verification: 31st International Conference, CA V 2019, New York City, NY, USA, July 15-18, 2019, Proc...

    2019

  36. [36]

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

    1982

  37. [37]

    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

    1973

  38. [38]

    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. doi:10.1145/ 2933575.2934518

    work page arXiv 2016

  39. [39]

    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

    1996

  40. [40]

    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

    2009

  41. [41]

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

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

  42. [42]

    D. S. Mitrinovic. 1970. Analytic Inequalities. Springer-Verlag. Proc. ACM Program. Lang., Vol. 0, No. POPL, Article 0. Publication date: May 2027. Quantitative Linear Logic 0:27

    1970

  43. [43]

    Marius Mosbach, Maksym Andriushchenko, Thomas Trost, Matthias Hein, and Dietrich Klakow. 2019. Logit Pairing Methods Can Fool Gradient-Based Attacks. doi: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

  44. [44]

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

    1998

  45. [45]

    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

  46. [46]

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

    1983

  47. [47]

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

    2023

  48. [48]

    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. doi:10.1145/1863543. 1863568

    work page doi:10.1145/1863543 2010

  49. [49]

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

    2026

  50. [50]

    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. In LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023 (EPiC Series in Comput...

    work page doi:10.29007/c1nt 2023

  51. [51]

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

  52. [52]

    Intriguing properties of neural networks

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

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

  53. [53]

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

    work page doi:10.1016/j.tcs.2004.09.035 2005

  54. [55]

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

    work page doi:10.1016/j.artint.2021.103602 2022

  55. [56]

    Dimarogonas

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

    work page doi:10.23919/acc45564.2020.9147692 2020

  56. [57]

    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

  57. [58]

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

    work page doi:10.1016/0165-0114(80)90013-5 1980

  58. [59]

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

    1965

  59. [60]

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

    1988

  60. [61]

    J Łukasiewicz. 1920. O logice trójwartościowej (in Polish). English translation: On Three-Valued Logic, in Borkowski, L.(ed.)

    1920

  61. [62]

    Ruch Filozoficzny

    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) (𝑏 ⊸ 𝑎) ⊗ ( 𝑐 ⊸ 𝑏) ≤ ( 𝑐 ⊸ 𝑎), (3) (𝑏 ⊸ 𝑎) ⊗ ( 𝑑 ⊸ 𝑐) ≤ ( 𝑏 ⊗ 𝑑) ⊸ (𝑎 ⊗ 𝑐), (4) 𝑎 ⊸ (𝑏 ⊸ 𝑐) = (𝑎 ⊗ 𝑏) ⊸ 𝑐. Proof. For (1), start from 1 ⊗ 𝑎 ≤ 𝑎∗∗ ...

    2027