dmxlarchey / relevant-decidability

A constructive account of Kripke-Curry's decidability proof for Implicational Relevance logic (see README.md below)

A Constructive Mechanization of Kripke-Curry's method for the Decidability of Implicational Relevance Logic

    (**************************************************************)
    (*   Copyright Dominique Larchey-Wendling [*]                 *)
    (*                                                            *)
    (*                             [*] Affiliation LORIA -- CNRS  *)
    (**************************************************************)
    (*      This file is distributed under the terms of the       *)
    (*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
    (**************************************************************)

What is this repository for?

• This repository is a companion Coq development for the paper Constructive Decision via Redundancy-free Proof-Search by Dominique Larchey-Wendling. The paper has been presented at IJCAR 2018. A revised and extended version of this paper is going to appear in the Journal of Automated Reasonning (JAR).

• The Coq mechanization of the decidability proof for Implicational Relevance logic is purely constructive, replacing Kripke/Dickson's lemma and König's lemma by inductive counterparts based on the notion of Almost Full relations.

• The code in sync the IJCAR 2018 publication is tagged v1.0.

• The code in sync with the JAR 2020 publication is tagged v2.0.

How do I get a set up?

• Using Coq 8.8+ (see below), compile this repository with make all (or make -j 16 all if you have 16 CPU cores available) and you can then review the proofs using your favorite Coq IDE. The file you want to review first in logical_deciders.v.

• Compilation was tested thoroughly and should work under the following versions of Coq: Coq 8.8.2, Coq 8.9.1 and Coq 8.10.1. However, cleaning up with make clean might be necessary when switching to another version of Coq.

• This repository was initially designed under Coq 8.6.1. However, due to changes in more recent versions of Coq, e.g. the Focus command being marked deprecated, the code has been updated and should now be compiled starting with Coq 8.8.

relevant-decidability's Issues

Actual licence of this software?

Hi,

I would like to use this library for one of my developments. I am interested by the tree induction principle that you introduced in one of your email on the Coq mailing list, and then in Kruskal and then this repo.

There are two license files in place, one is LGPL, the other is CeCiLLv2. However, it seems all files are released under CeCiLLv2 only,. Is this correct? Can you confirm all files are released under this license?

Thanks,