Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions

Guy Perrier 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Given an intuitionistic proof net of linear logic, we abstract an order between its atomic formulas. From this order, we represent intuitionistic multiplicative proof nets in the more compact form of models of directed acyclic graph descriptions. If we restrict the logical framework to the implicative fragment of intuitionistic linear logic, we show that proof nets reduce to models of tree descriptions.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00100667
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 2:48:50 PM
Last modification on : Thursday, January 11, 2018 - 6:19:48 AM

Identifiers

  • HAL Id : inria-00100667, version 1

Collections

Citation

Guy Perrier. Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions. 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning - LPAR 2001, 2001, Havana, Cuba, France. pp.233-248. ⟨inria-00100667⟩

Share

Metrics

Record views

230