Hypersequents and Systems of Rules: Embeddings and Applications

Abstract

We define a bi-directional embedding between hypersequent calculi and a subclass of systems of rules (2-systems). In addition to showing that the two proof frameworks have the same expressive power, the embedding allows for the recovery of the benefits of locality for 2-systems, analyticity results for a large class of such systems, and a rewriting of hypersequent rules as natural deduction rules.

32 pages, the final publication is available at ACM DL via https://dl.acm.org/citation.cfm?id=3180075