A method of marks and indices for linear modal logic

Abstract

In the paper a method to check termination of history-free proof for linear modal logic S4.3 is proposed. This method improves the method proposed by the authors for modal logic S4. Analogously as for S4, instead of history we use marks and indices that allow us to eliminate loop checking. The method proposed in this paper specifies some kind of formulas which allow us to check termination of derivations in more effective way in comparison with S4.

Keywords

• modal logics
• sequent calculus
• termination
• invertible rules