Artifact
Formalisation of Differentiable Logics in Coq Software
Authors
Natalia Ślusarz 
,
Reynald Affeldt ,
Alessandro Bruni
- Part of: Collection: Supplementary Materials
- License: MIT License
- Publication Date: 2024-11-28
Author Details
Content
- Software (Source): https://github.com/ndslusarz/formal_LDL
-
archived version
Version/Status
- Content created at: 2023-04-21
- Status: Active (at the time of publication 2024-11-28)
Description
This repository contains the formalization of the Logic of Differentiable Logics (LDL) using the Coq proof-assistant and the Mathematical Components library. The LDL language is defined in ldl.v, along with its fuzzy, DL2, STL and Boolean interpretations. The files fuzzy.v, dl2.v, dl2_ereal.v, stl.v and stl_ereal.v contain the relevant theorems that hold for each interpretation: structural properties (idempotence, commutativity and associativity of operators), soundness, and shadow-lifting. The files mathcomp_extra.v and analysis_extra.v contain extra lemmas related to the respective libraries, including L'Hopital and Cauchy MVT in the latter.
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)