Formalisation of Differentiable Logics in Coq

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.

Meta

• Author(s):
  • Natalia Slusarz (initial)
  • Reynald Affeldt (initial)
  • Alessandro Bruni (initial)
• License: MIT License
• Compatible Coq versions: 8.18 to 8.19
• Additional dependencies:
  • MathComp 2.2.0
  • MathComp Analysis 1.3.1
  • MathComp Algebra Tactics 1.2.3
• Related publication(s):
  • Taming Differentiable Logics with Coq Formalisation

Building and installation instructions

The easiest way to install the latest released version of Formalisation of Differentiable Logics in Coq is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-formal-LDL

To instead build and install manually, do:

git clone https://github.com/ndslusarz/formal-LDL.git
cd formal-LDL
make   # or make -j <number-of-cores-on-your-machine> 
make install