TY - GEN
T1 - Correspondence between modal Hilbert axioms and sequent rules with an application to S5
AU - Lellmann, Björn
AU - Pattinson, Dirk
PY - 2013
Y1 - 2013
N2 - Which modal logics can be 'naturally' captured by a sequent system? Clearly, this question hinges on what one believes to be natural, i.e. which format of sequent rules one is willing to accept. This paper studies the relationship between the format of sequent rules and the corresponding syntactical shape of axioms in an equivalent Hilbert-system. We identify three different such formats, the most general of which captures most logics in the S5-cube. The format is based on restricting the context in rule premises and the correspondence is established by translating axioms into rules of our format and vice versa. As an application we show that there is no set of sequent rules of this format which is sound and cut-free complete for S5 and for which cut elimination can be shown by the standard permutation-of-rules argument.
AB - Which modal logics can be 'naturally' captured by a sequent system? Clearly, this question hinges on what one believes to be natural, i.e. which format of sequent rules one is willing to accept. This paper studies the relationship between the format of sequent rules and the corresponding syntactical shape of axioms in an equivalent Hilbert-system. We identify three different such formats, the most general of which captures most logics in the S5-cube. The format is based on restricting the context in rule premises and the correspondence is established by translating axioms into rules of our format and vice versa. As an application we show that there is no set of sequent rules of this format which is sound and cut-free complete for S5 and for which cut elimination can be shown by the standard permutation-of-rules argument.
UR - http://www.scopus.com/inward/record.url?scp=84885718900&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-40537-2_19
DO - 10.1007/978-3-642-40537-2_19
M3 - Conference contribution
AN - SCOPUS:84885718900
SN - 9783642405365
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 219
EP - 233
BT - Automated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings
T2 - 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013
Y2 - 16 September 2013 through 19 September 2013
ER -