Sciweavers

Share
LICS
2012
IEEE

Countermodels from Sequent Calculi in Multi-Modal Logics

6 years 10 months ago
Countermodels from Sequent Calculi in Multi-Modal Logics
—A novel countermodel-producing decision procedure that applies to several multi-modal logics, both intuitionistic and classical, is presented. Based on backwards search in labeled sequent calculi, the procedure employs a novel termination condition and countermodel construction. Using the procedure, it is argued that multi-modal variants of several classical and intuitionistic logics including K, T, K4, S4 and their combinations with D are decidable and have the finite model property. At least in the intuitionistic multi-modal case, the decidability results are new. It is further shown that the countermodels produced by the procedure, starting from a set of hypotheses and no goals, characterize the atomic formulas provable from the hypotheses.
Deepak Garg, Valerio Genovese, Sara Negri
Added 29 Sep 2012
Updated 29 Sep 2012
Type Journal
Year 2012
Where LICS
Authors Deepak Garg, Valerio Genovese, Sara Negri
Comments (0)
books