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.
Hypersequents and Systems of Rules / A. Ciabattoni, F.A. Genco. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - 19:2(2018), pp. 1-27. [10.1145/3180075]
Hypersequents and Systems of Rules
F.A. GencoUltimo
2018
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.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
TOCL.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
570.63 kB
Formato
Adobe PDF
|
570.63 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.