Proof-nets are special graphs (proof-structures) representing desequentialised proofs of the linear logic sequent calculus. Each proof-net stands for a class of sequent proofs which are equivalent modulo irrelevant permutations of logical rules. Here we present an interactive characterisation of those cut-free proof-structures coming from proofs of the multiplicative-additive fragment of linear logic (MALL, see [1, 3]). This work is intended to extend to MALL proof-nets an original proposal for an interactive correction criterion for proof-nets of the multiplicative fragment of linear logic. Its natural consequence we will be the study of the question of modularity for additive proof-nets.
Maieli, R., Ruet, P. (2006). Interactive correctness criterion for multiplicative-additive proof-nets. In Proceedings of the Twenty-First Annual IEEE Symposium (LICS 2006). IEEE Computer Society.
Interactive correctness criterion for multiplicative-additive proof-nets
MAIELI, ROBERTO;
2006-01-01
Abstract
Proof-nets are special graphs (proof-structures) representing desequentialised proofs of the linear logic sequent calculus. Each proof-net stands for a class of sequent proofs which are equivalent modulo irrelevant permutations of logical rules. Here we present an interactive characterisation of those cut-free proof-structures coming from proofs of the multiplicative-additive fragment of linear logic (MALL, see [1, 3]). This work is intended to extend to MALL proof-nets an original proposal for an interactive correction criterion for proof-nets of the multiplicative fragment of linear logic. Its natural consequence we will be the study of the question of modularity for additive proof-nets.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
