Proof nets are a parallel syntax for sequential proofs of linear logic, firstly introduced by Girard in 1987. Here we present and intrinsic (geometrical) characterization of proof nets, that is a correctness criterion (an algorithm) for checking those proof structures which correspond to proofs of the purely multiplicative and additive fragment of linear logic. This criterion is formulated in terms of simple graph rewriting rules and it extends an initial idea of a retraction correctness criterion for proof nets of the purely multiplicative fragment of linear logic presented by Danos in his Thesis in 1990.

Maieli, R. (2007). Retractile Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic. In Logic for Programming, Artificial Intelligence, and Reasoning. - 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007. Proceedingsasoning. (pp.363-377). BERLIN HEIDELBERG : Springer-Verlag [10.1007/978-3-540-75560-9_27].

Retractile Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic

MAIELI, ROBERTO
2007

Abstract

Proof nets are a parallel syntax for sequential proofs of linear logic, firstly introduced by Girard in 1987. Here we present and intrinsic (geometrical) characterization of proof nets, that is a correctness criterion (an algorithm) for checking those proof structures which correspond to proofs of the purely multiplicative and additive fragment of linear logic. This criterion is formulated in terms of simple graph rewriting rules and it extends an initial idea of a retraction correctness criterion for proof nets of the purely multiplicative fragment of linear logic presented by Danos in his Thesis in 1990.
978-3-540-75558-6
Maieli, R. (2007). Retractile Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic. In Logic for Programming, Artificial Intelligence, and Reasoning. - 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007. Proceedingsasoning. (pp.363-377). BERLIN HEIDELBERG : Springer-Verlag [10.1007/978-3-540-75560-9_27].
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/160438
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 3
social impact