Coq formalisation of linear nested sequents for the tense logic Kt.
By Caitlin D'Abrera, Jeremy Dawson and Rajeev Gore.
The general directory contains files for encoding derivability and other generic system non-specific results.
The tense-lns directory contains encodings of LNS for tense logic and its related proofs, e.g. cut-eliminiation.
To use, see tense-lns/README.txt.
Tested on Coq 8.10.2 (November, 2019)