The logics CK and WK are two fundamental systems of constructive modal logics, which aim to provide an interpretation of modalities with an intuitionistic base. Semantics of these logics can be specified in terms of bi-relational models. We define bi-nested sequent calculi for these two systems. Our calculi are cut-free and only consist of invertible rules. Moreover, they support terminating proof-search under a suitable strategy. The main feature of the calculi is that they allow to directly construct countermodels in the bi-relational semantics from any failed proof.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Constructive Modal Logics: Bi-nested Calculi and Bi-relational Countermodels

  • Han Gao,
  • Nicola Olivetti

摘要

The logics CK and WK are two fundamental systems of constructive modal logics, which aim to provide an interpretation of modalities with an intuitionistic base. Semantics of these logics can be specified in terms of bi-relational models. We define bi-nested sequent calculi for these two systems. Our calculi are cut-free and only consist of invertible rules. Moreover, they support terminating proof-search under a suitable strategy. The main feature of the calculi is that they allow to directly construct countermodels in the bi-relational semantics from any failed proof.