Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version)
Logic in Computer Science
2019-07-03 v1
Abstract
We give a linear nested sequent calculus for the basic normal tense logic Kt. We show that the calculus enables backwards proof-search, counter-model construction and syntactic cut-elimination. Linear nested sequents thus provide the minimal amount of nesting necessary to provide an adequate proof-theory for modal logics containing converse. As a bonus, this yields a cut-free calculus for symmetric modal logic KB.
Keywords
Cite
@article{arxiv.1907.01270,
title = {Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version)},
author = {Rajeev Goré and Björn Lellmann},
journal= {arXiv preprint arXiv:1907.01270},
year = {2019}
}
Comments
Extended version of the paper accepted at TABLEAUX2019, containing an additional technical appendix