A formally verified cut-elimination procedure for linear nested sequents for tense logic (Q2142082)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A formally verified cut-elimination procedure for linear nested sequents for tense logic |
scientific article |
Statements
A formally verified cut-elimination procedure for linear nested sequents for tense logic (English)
0 references
25 May 2022
0 references
formalised proof theory
0 references
cut-elimination
0 references
linear nested sequent calculus
0 references
tense logic
0 references
Coq
0 references
extraction
0 references
program synthesis
0 references
