Reference. Quantifiers for Differentiable Logics in Rocq (Extended Abstract)

Cite

Cite as @marulandagiraldo-2025-quantifiers (helia, typst) · \cite{marulandagiraldo-2025-quantifiers} (LaTeX)
BibTeX
bibtex · 1 line
@inbook{marulandagiraldo-2025-quantifiers, title={Quantifiers for Differentiable Logics in Rocq (Extended Abstract)}, ISBN={9783031999918}, ISSN={1611-3349}, url={http://dx.doi.org/10.1007/978-3-031-99991-8_12}, DOI={10.1007/978-3-031-99991-8_12}, booktitle={AI Verification}, publisher={Springer Nature Switzerland}, author={Marulanda-Giraldo, Jairo Miguel and Komendantskaya, Ekaterina and Bruni, Alessandro and Affeldt, Reynald and Capucci, Matteo and Marchioni, Enrico}, year={2025}, month=Oct, pages={227–237} }
hayagriva YAML (typst)
yaml · 21 lines
marulandagiraldo-2025-quantifiers:
  type: chapter
  title: Quantifiers for Differentiable Logics in Rocq (Extended Abstract)
  author:
  - Marulanda-Giraldo, Jairo Miguel
  - Komendantskaya, Ekaterina
  - Bruni, Alessandro
  - Affeldt, Reynald
  - Capucci, Matteo
  - Marchioni, Enrico
  date: 2025-10
  page-range: 227-237
  url: http://dx.doi.org/10.1007/978-3-031-99991-8_12
  serial-number:
    doi: 10.1007/978-3-031-99991-8_12
    isbn: '9783031999918'
    issn: 1611-3349
  parent:
    type: book
    title: AI Verification
    publisher: Springer Nature Switzerland
Cites 25 works (1 here)
With notes (1)

On Quantifiers for Quantitative Reasoning capucci-2024-on

We explore a kind of first-order predicate logic with intended semantics in the reals. Compared to other approaches in the literature, we work predominantly in the multiplicative reals [0,∞], showing they support three generations of connectives, that we call non-linear, linear additive, and linear multiplicative. Means and harmonic means emerge as natural candidates for bounded existential and universal quantifiers, and in fact we see they behave as expected in relation to the other logical connectives. We explain this fact through the well-known fact that min/max and arithmetic mean/harmonic mean sit at opposite ends of a spectrum, that of p-means. We give syntax and semantics for this quantitative predicate logic, and as example applications, we show how softmax is the quantitative semantics of argmax, and Rényi entropy/Hill numbers are additive/multiplicative semantics of the same formula. Indeed, the additive reals also fit into the story by exploiting the Napierian duality −log⊣1/exp, which highlights a formal distinction between ‘additive’ and ‘multiplicative’ quantities. Finally, we describe two attempts at a categorical semantics via enriched hyperdoctrines. We discuss why hyperdoctrines are in fact probably inadequate for this kind of logic.
DOI · arXiv
External (24)
marulandagiraldo-2025-quantifiers reference entries/refs/marulandagiraldo-2025-quantifiers/marulandagiraldo-2025-quantifiers.hel