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. © 2012 IEEE.
Countermodels from sequent calculi in multi-modal logics
Negri S.
2012-01-01
Abstract
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. © 2012 IEEE.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
