Взаимное преобразование секвенциальных и натуральных выводов в модальной логике.

Abstract

Constructive method of mutual transformation of sequent and natural deductions in modal systems is presented. The procedure of transformation is illustrated using two propositional modal systems \textbf{GS5} and \textbf{NS5} . The first is sequent calculus with global versions of modal inference rules. The second is natural deduction system with marked occurences of formulae. This method can be applied to various so called normal modal systems, particulary to the systems which are extensions of \textbf{S4} and at the same time subsystems of \textbf{S5} .