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. Genco
Ultimo
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.
embedding between formalisms; Hypersequents; intermediate logics; natural deduction; systems of rules;
Settore M-FIL/02 - Logica e Filosofia della Scienza
2018
Article (author)
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/1036352
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 4
social impact