Formalisation of Differentiable Logics

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, STLinfty and Boolean interpretations. The files fuzzy.v, dl2.v, dl2_ereal.v, stl.v, stl_ereal.v and stl_infty.v contain the relevant theorems that hold for each interpretation: structural properties based on residuated lattices (idempotence, commutativity and associativity of operators, residuation, prelinearity etc.), adequacy, and shadow-lifting.

The formalisation of soundness of hypersequent calculi for fuzzy logics can be found in file seq_calc.v, for DL2 in dl2_seq_calc.v and for STLinfty in stl_infty_seq_calc.v.

Meta

• Author(s):
  • Reynald Affeldt (initial)
  • Alessandro Bruni (initial)
  • Natalia Ślusarz (initial)
  • Kathrin Stark (initial)
  • Ekaterina Komendantskaya (initial)
• License: MIT License
• Compatible Rocq/Coq versions: 8.20 or later
• Additional dependencies:
  • MathComp 2.4.0
  • MathComp Analysis 1.12.0
  • MathComp Algebra Tactics 1.2.5
• 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 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/formal-LDL/formal-LDL.git
cd formal-LDL
make   # or make -j <number-of-cores-on-your-machine> 
make install