Content

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

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail