Skip Navigation

Logic Journal of IGPL 2005 13(2):173-199; doi:10.1093/jigpal/jzi013
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Mateus, P.
Right arrow Articles by Sernadas, C.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2005. Published by Oxford University Press. All rights reserved.

Original Articles

Modal Sequent Calculi Labelled with Truth Values: Cut Elimination

Paulo Mateus1, João Rasga2 and Cristina Sernadas3

1 CLC, Departamento de Matemática, IST, Av. Rovisco Pais, 1049-001, Lisboa, Portugal. E-mail: pmat{at}math.ist.utl.pt, 2 CLC, Departamento de Matemática, IST, Av. Rovisco Pais, 1049-001, Lisboa, Portugal. E-mail: jfr{at}math.ist.utl.pt, 3 CLC, Departamento de Matemática, IST, Av. Rovisco Pais, 1049-001, Lisboa, Portugal. E-mail: css{at}math.ist.utl.pt

Cut elimination is shown, in a constructive way, to hold in sequent calculi labelled with truth values for a wide class of normal modal logics, supporting global and local reasoning and allowing a general frame semantics. The complexity of cut elimination is studied in terms of the increase of logical depth of the derivations. A hyperexponential worst case bound is established. The subformula property and a similar property for the label terms are shown to be satisfied by that class of modal sequent calculi. Modal logics presented by these calculi are proven to be globally and locally consistent.

Key Words: Cut elimination, complexity of cut elimination, modal sequent calculus, labelled deduction

Received 26 July 2004. Revised 12 January 2005.


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer: Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.