A method of marks and indices for linear modal logic
Articles
Regimantas Pliuškevičius
Institute of Mathematics and Informatics
Aida Pliuškevičienė
Institute of Mathematics and Informatics
Published 2009-12-20
https://doi.org/10.15388/LMR.2009.48
PDF

Keywords

modal logics
sequent calculus
termination
invertible rules

How to Cite

Pliuškevičius R. and Pliuškevičienė A. (2009) “A method of marks and indices for linear modal logic”, Lietuvos matematikos rinkinys, 50(proc. LMS), pp. 269–274. doi: 10.15388/LMR.2009.48.

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.

PDF
Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

Please read the Copyright Notice in Journal Policy