A formally verified cut-elimination procedure for linear nested sequents for tense logic
scientific article