Coq formalisation of cut-elimination via backward proof-search for GLS.
By Rajeev Goré, Revantha Ramanayake and Ian Shillito.
The general directory contains files for encoding derivability and other generic system non-specific results.
The GL directory contains encodings of a sequent calculus for provability logic GL and its related proofs, e.g. cut-eliminiation.
To use, see GL/README.md.
Tested on Coq 8.11.2 (June, 2020)