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

January 28, 2020 · View on GitHub

    (**************************************************************)
    (*   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.