A computational interpretation of modal proofs

The authors consider some computational properties of intuitionistic 2-sequent calculus [see A. Masini, J. Logic Comput. 3 (1993), no. 5, 533--562; MR1253870 (95d:03030)] and of the positive fragments of the modal systems K4, KT and S4, for which corresponding natural deduction systems are introduced. The inference rules of these systems act only on the conclusions and/or the premises of deductions they are applied to, no introduction inference rule has a premise containing the introduced connective, and the modal rules strictly match the usual rules for the universal quantifier (the side conditions on variables become a side condition on levels). Such a definition of systems makes it possible to differentiate the logics under consideration using only one parameter of the elimination rule for the necessity operator and to compare them clearly with respect to the known semantical properties of Kripke frames. A strongly normalizing and confluent reduction procedure, based on β-reduction for λ-terms and defined on the terms representing proofs, enables one to obtain a natural computational interpretation for proofs; this is the central point of the paper. This approach to the theory of formal logical systems opens up new views on the subject