FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Constructive Decision via Redundancy-free Proof-Search

Author: Dominique Larchey-Wendling

Paper Information

Title:Constructive Decision via Redundancy-free Proof-Search
Authors:Dominique Larchey-Wendling
Proceedings:IJCAR Proceedings 9th IJCAR, 2018
Editors: Stephan Schulz, Didier Galmiche and Roberto Sebastiani
Keywords:Constructive Decidability, Relevance Logic, Redundancy-free Proof-Search, Almost Full relations
Abstract:

ABSTRACT. We give a constructive account of Kripke-Curry's method which was used to establish the decidability of Implicational Relevance Logic (R->). To sustain our approach, we mechanize this method in axiom-free Coq, abstracting away from the specific features of R-> to keep only the essential ingredients of the technique. In particular we show how to replace Kripke/Dickson's lemma by a constructive form of Ramsey's theorem based on the notion of almost full relation. We also explain how to replace König's lemma with an inductive form of Brouwer's Fan theorem. We instantiate our abstract proof to get a constructive decision procedure for R-> and discuss potential applications to other logical decidability problems.

Pages:16
Talk:Jul 15 11:00 (Session 103D: Formal Proofs)
Paper: