Open AccessContraction-free calculi for modal logics S5 and KD45
Author(s) -
Julius Andrikonis,
Regimantas Pliuškevičius
Publication year - 2011
Publication title -
lietuvos matematikos rinkinys
Language(s) - English
Resource type - Journals
eISSN - 2335-898X
pISSN - 0132-2818
DOI - 10.15388/lmr.2011.ml03
Subject(s) - sequent , modal , mathematics , natural deduction , sequent calculus , axiom , backtracking , modality (human–computer interaction) , calculus (dental) , t norm fuzzy logics , mathematical economics , computer science , algorithm , discrete mathematics , artificial intelligence , geometry , mathematical proof , medicine , fuzzy set , polymer chemistry , chemistry , dentistry , membership function , fuzzy logic
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.