Tree-sequent calculi and decision procedures for intuitionistic modal logics

2015 ◽  
Vol 28 (5) ◽  
pp. 967-989 ◽  
Author(s):  
Didier Galmiche ◽  
Yakoub Salhi
Keyword(s):  
Decision Procedures ◽  
Modal Logics ◽  
Sequent Calculi ◽  
Intuitionistic Modal Logics

Gentzen sequent calculi for some intuitionistic modal logics

2019 ◽  
Vol 27 (4) ◽  
pp. 596-623
Author(s):  
Zhe Lin ◽  
Minghui Ma
Keyword(s):  
Propositional Logic ◽  
Sequent Calculus ◽  
Modal Logics ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Intuitionistic Propositional Logic ◽  
Propositional Language ◽  
Intuitionistic Modal Logics ◽  
Subformula Property ◽  
Gentzen Sequent Calculus

Abstract Intuitionistic modal logics are extensions of intuitionistic propositional logic with modal axioms. We treat with two modal languages ${\mathscr{L}}_\Diamond $ and $\mathscr{L}_{\Diamond ,\Box }$ which extend the intuitionistic propositional language with $\Diamond $ and $\Diamond ,\Box $, respectively. Gentzen sequent calculi are established for several intuitionistic modal logics. In particular, we introduce a Gentzen sequent calculus for the well-known intuitionistic modal logic $\textsf{MIPC}$. These sequent calculi admit cut elimination and subformula property. They are decidable.

Modular Sequent Calculi for Classical Modal Logics

Studia Logica ◽  
2014 ◽  
Vol 103 (1) ◽  
pp. 175-217 ◽  
Author(s):  
David R. Gilbert ◽  
Paolo Maffezioli
Keyword(s):  
Modal Logics ◽  
Sequent Calculi
Sign in / Sign up

Export Citation Format

Share Document