Taming differentiable logics with Coq formalisation

DOI10.4230/LIPICS.ITP.2024.4MaRDI QIDQ6860035zbMATH OpenFDO

Authors Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, Kathrin Stark

Publication date 10 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2024.4

zbMATH Keywords

differentiable logicsinteractive theorem provinglogic and semanticsloss functionsmachine learning

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• Analyzing differentiable fuzzy logic operators
• Formalization techniques for asymptotic reasoning in classical analysis
• Logic of differentiable logics: towards a uniform semantics of DL
• Propositional logics for the Lawvere quantale
• Reflexive tactics for algebra, revisited
• Verifying feedforward neural networks for classification in Isabelle/HOL

Cited in

(1)

• Proof-carrying neuro-symbolic code

This page was built for publication: Taming differentiable logics with Coq formalisation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6860035)