Search

In the article, loop-free calculus for modal logic S4 is presented. To restrict applications of reflexivity and transitivity rules, several types of indexes are used. The use of indexes replaces the need to keep the history of previous applications of the rules. The article details the purpose of each type of index and proves that derivation search in the calculus is finite.

We analyze the multimodal logic S4n with the central agent axiom. We present a Hilbert-type calculus, then derive a Gentzen-type calculus with cut, and prove a cut-elimination theorem. The work shows that it is possible to construct a cut-free Gentzen-type calculus for this logic. Moreover, it also provides analogous results for the multimodal logic K4n with the central agent axiom.

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.