It is now well-established that the so-called focalization property plays a central role in the design of programming languages based on proof search, and more generally in the proof theory of linear logic. We present here a sequent calculus for non-commutative logic (NL) which enjoys the focalization property. In the multiplicative case, we give a focalized sequentialization theorem, and in the general case, we show that our focalized sequent calculus is equivalent to the original one by studying the permutabilities of rules for NL and showing that all permutabilities of linear logic involved in focalization can be lifted to NL permut- abilities. These results are based on a study of the partitions of partially ordered sets modulo entropy.

Maieli, R., Ruet, P. (2003). Non-commutative logic III : focusing proofs. INFORMATION AND COMPUTATION, 185(2), 233-262 [10.1016/S0890-5401(03)00084-1].

Non-commutative logic III : focusing proofs

MAIELI, ROBERTO
;
2003-01-01

Abstract

It is now well-established that the so-called focalization property plays a central role in the design of programming languages based on proof search, and more generally in the proof theory of linear logic. We present here a sequent calculus for non-commutative logic (NL) which enjoys the focalization property. In the multiplicative case, we give a focalized sequentialization theorem, and in the general case, we show that our focalized sequent calculus is equivalent to the original one by studying the permutabilities of rules for NL and showing that all permutabilities of linear logic involved in focalization can be lifted to NL permut- abilities. These results are based on a study of the partitions of partially ordered sets modulo entropy.
2003
Maieli, R., Ruet, P. (2003). Non-commutative logic III : focusing proofs. INFORMATION AND COMPUTATION, 185(2), 233-262 [10.1016/S0890-5401(03)00084-1].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/11590/144264
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 3
social impact