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.
Mots-clés : linear logic réseaux de démonstration logique linéaire proof nets
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

INRIA | CNRS | LORIA | UNIV-LORRAINE

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

230

 

 

Contact

archive-ouverte@inria.fr