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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.