A computational interpretation of modal proofs

@incollection{citeulike:2629697, abstract = {The usual (e.g. Prawitz's) treatment of natural deduction for modal logics involves a complicated rule for the introduction of the necessity, since the naive one does not allow normalization. We propose natural deduction systems for the positive fragments of the modal logics K, K4, KT, and S4, extending previous work by Masini on a two-dimensional generalization of Gentzen's sequents (2-sequents). The modal rules closely match the standard rules for an universal quantifier and different logics...}, author = {Martini, S. and Masini, A. }, booktitle = {Proof Theory of Modal Logics}, citeulike-article-id = {2629697}, editor = {Wansing, H. }, keywords = {lambda-calculi, modal-logic}, posted-at = {2008-04-04 15:03:49}, priority = {2}, publisher = {Kluwer}, title = {A computational interpretation of modal proofs}, url = {http://citeseer.ist.psu.edu/martini94computational.html}, year = {1995} }

TY - CHAP ID - citeulike:2629697 L3 - citeulike-article-id:2629697 TI - A computational interpretation of modal proofs T2 - Proof Theory of Modal Logics PB - Kluwer N2 - The usual (e.g. Prawitz's) treatment of natural deduction for modal logics involves a complicated rule for the introduction of the necessity, since the naive one does not allow normalization. We propose natural deduction systems for the positive fragments of the modal logics K, K4, KT, and S4, extending previous work by Masini on a two-dimensional generalization of Gentzen's sequents (2-sequents). The modal rules closely match the standard rules for an universal quantifier and different logics... KW - lambda-calculi KW - modal-logic AU - Martini, S AU - Masini, A A2 - Wansing, H PY - 1995/// UR - http://citeseer.ist.psu.edu/martini94computational.html ER -