{
    "@context": "https:\/\/doi.org\/10.5063\/schema\/codemeta-2.0",
    "@type": "SoftwareSourceCode",
    "codeRepository": "https:\/\/github.com\/ndslusarz\/formal_LDL",
    "author": [
        {
            "@type": "Person",
            "givenName": "Natalia",
            "familyName": "\u015alusarz",
            "email": "natalia.d.slusarz@gmail.com",
            "affiliation": {
                "@type": "Organization",
                "name": "Heriot-Watt University"
            },
            "@id": "https:\/\/orcid.org\/0000-0001-5729-9208"
        },
        {
            "@type": "Person",
            "givenName": "Reynald",
            "familyName": "Affeldt",
            "affiliation": {
                "@type": "Organization",
                "name": "National Institute of Advanced Industrial Science and Technology(AIST)"
            },
            "@id": "https:\/\/orcid.org\/0000-0002-2327-953X",
            "email": "reynald.affeldt@gmail.com"
        },
        {
            "@type": "Person",
            "givenName": "Alessandro",
            "familyName": "Bruni",
            "affiliation": {
                "@type": "Organization",
                "name": "IT-University of Copenhagen"
            },
            "email": "brun@itu.dk",
            "@id": "https:\/\/orcid.org\/0000-0003-2946-9462"
        }
    ],
    "name": "Formalisation of Differentiable Logics in Coq",
    "programmingLanguage": "Coq",
    "license": "https:\/\/spdx.org\/licenses\/MIT.html",
    "developmentStatus": "Active",
    "dateCreated": "2023-04-21",
    "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.",
    "identifier": "https:\/\/archive.softwareheritage.org\/swh:1:dir:bd213b761dfc453ccfe8e785a38cffe583c98f04;origin=https:\/\/github.com\/ndslusarz\/formal_LDL;visit=swh:1:snp:b2cb2b91dfa180cde7ca3a5ee8e013e02c3cbd5a;anchor=swh:1:rev:bd0e5eddeae0d264b736fdd1bbb9edd4e8fe1a99",
    "datePublished": "2024-11-28"
}