Contraction-free calculi for modal logics S5 and KD45
Articles
Julius Andrikonis
Vilnius University
Regimantas Pliuškevičius
Vilnius University
Published 2011-12-15
https://doi.org/10.15388/LMR.2011.ml03
PDF

Keywords

modal logic
sequent calculus
termination
backtracking
contraction-free

How to Cite

Andrikonis, J. and Pliuškevičius, R. (2011) “Contraction-free calculi for modal logics S5 and KD45”, Lietuvos matematikos rinkinys, 52(proc. LMS), pp. 237–242. doi:10.15388/LMR.2011.ml03.

Abstract

It is known that termination and backtracking are among the most important problems in constructing derivations in non-classical logics. In this paper contractionfree and backtracking-free sequent calculi for modal logics S5 and KD45 are presented and founded. These are index-style sequent calculi with some specific indexed axioms. The main new ideas in considered calculi are to use metavariables (along with natural numbers) as elements of indexes and to numerate by different natural number all the positive occurrences of modality 2.

PDF

Downloads

Download data is not yet available.