Specialization of derivations in modal logic S5

Abstract

Loop-check-free decidable specialization of sequent calculus for modal logic S5 is presented. Soundness and completness of this calculus is proved.

Keywords

• modal logic
• sequent calculus
• decidable calculus
• loop-check