Countermodel Construction via Optimal Hypersequent Calculi for Non-normal Modal Logics

Björn Lellmann (1) , Nicola Olivetti (2, 3) , Elaine Pimentel (4) , Tiziano Dalmonte (5, 3)

1 TU Wien - Vienna University of Technology
2 LIS - Laboratoire d'Informatique et Systèmes
3 LIRICA - Logique, Interaction, Raisonnement et Inférence, Complexité, Algèbre
4 UFRN - Universidade Federal do Rio Grande do Norte [Natal]
5 LSIS - Laboratoire des Sciences de l'Information et des Systèmes

We develop semantically-oriented calculi for the cube of non-normal modal logics and some deontic extensions. The calculi manipulate hypersequents and have a simple semantic interpretation. Their main feature is that they allow for direct countermodel extraction. Moreover they provide an optimal decision procedure for the respective logics. They also enjoy standard proof-theoretical properties, such as a syntactical proof of cut-admissibility.

Keywords: Non-normal modal logics; Hypersequents; Countermodel con- struction; Cut elimination

Domains: Computer Science [cs]; Computer Science [cs]; Logic in Computer Science [cs.LO]; Computer Science [cs]; Artificial Intelligence [cs.AI]

Björn Lellmann, Nicola Olivetti, Elaine Pimentel, Tiziano Dalmonte. Countermodel Construction via Optimal Hypersequent Calculi for Non-normal Modal Logics. Logical Foundations of Computer Science - International Symposium, LFCS 2020, Jan 2020, Deerfield Beach, United States. ⟨hal-02436312⟩