Formalisation of Differentiable Logics in Coq

Ślusarz, Natalia; Affeldt, Reynald; Bruni, Alessandro

doi:10.4230/artifacts.22503

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

Document Identifiers

DOI: 10.4230/artifacts.22503
URN: urn:nbn:de:0030-drops-225037

Author Details

Natalia Ślusarz

Heriot-Watt University

Reynald Affeldt

National Institute of Advanced Industrial Science and Technology(AIST)

Alessandro Bruni

IT-University of Copenhagen

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)

Cite As Get BibTex

Natalia Ślusarz, Reynald Affeldt, Alessandro Bruni. Formalisation of Differentiable Logics in Coq (Software, Source). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/artifacts.22503

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.

Subject Classification

Programming Languages

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

Metadata Views

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail