Talks and Poster Presentations (with Proceedings-Entry):
R. Goré, B. Lellmann:
"Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequents";
Talk: TABLEAUX 2019,
London, UK;
2019-09-03
- 2019-09-05; in: "Automated Reasoning with Analytic Tableaux and Related Methods. 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings",
S. Cerrito, A. Popescu (ed.);
Springer,
LNCS, vol.11714
(2019),
ISBN: 978-3-030-29025-2;
185
- 202.
English 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:
Modal logic, Proof theory, Linear nested sequents, Countermodels
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-030-29026-9_11
Created from the Publication Database of the Vienna University of Technology.