Awesome
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 withmake all
(ormake -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 inlogical_deciders.v
. -
Compilation was tested thoroughly and should work under the following versions of Coq:
Coq 8.8.2
,Coq 8.9.1
andCoq 8.10.1
. However, cleaning up withmake 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. theFocus
command being marked deprecated, the code has been updated and should now be compiled starting withCoq 8.8
.