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
Type de document :
Communication dans un congrès
Robert Nieuwenhuis, Andrei Voronkov. 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning - LPAR 2001, 2001, Havana, Cuba, France. Springer, 2250, pp.233-248, 2001, Lecture Notes in Artificial Intelligence
Liste complète des métadonnées
https://hal.inria.fr/inria-00100667
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:48:50
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48

Identifiants

  • HAL Id : inria-00100667, version 1

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Guy Perrier. Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions. Robert Nieuwenhuis, Andrei Voronkov. 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning - LPAR 2001, 2001, Havana, Cuba, France. Springer, 2250, pp.233-248, 2001, Lecture Notes in Artificial Intelligence. 〈inria-00100667〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

167

Contact


archive-ouverte@inria.fr