Sequents vs hypersequents for Åqvist systems

Abstract

Enhancing cut-free expressiveness through minimal structural additions to sequent calculus is a natural step. We focus on Åqvist’s system F with cautious monotonicity (CM), a deontic logic extension of S5, for which we define a sequent calculus employing (semi) analytic cuts. The transition to hypersequents is key to develop modular and cut-free calculi for F + (cm) and G, also supporting countermodel construction.

Publication
International Joint Conference on Automated Reasoning
Agata Ciabattoni
Agata Ciabattoni
Professor of Non-Classical Logics in Computer Science

Agata Ciabattoni is a full professor of non-classical logics in computer science. She is an expert in proof theory for non-classical logics and their applications in various fields. Among other things, she has been investigating proof theory for deontic logic, its applications in AI, connections to legal reasoning, and formalisation of the deontic reasoning of the Mı̄māmsā school of Indian philosophy.

Matteo Tesi
Matteo Tesi
PostDoc Researcher (Marie Curie Individual Fellowship)

Matteo’s research focuses on non-classical (modal, intermediate, and substructural) logics, structural proof theory and their philosophical applications. He has worked with sequent calculi and their generalizations (hypersequents, nested sequents, and labelled sequents) to offer analytic presentations of families of non-classical logics.