Proof construction in linear logic and programming

Didier Galmiche 1
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this talk, we consider the problem to have efficient methods to construct proofs and proof nets in different fragments of Linear Logic (LL). Non-classical logics as intuitionistic and linear logics are used in various branches of computer science, through various programming paradigms like proof-search as computation, proofs-as-programs, proofs-as-computation, and then automated proof search (construction) methods are necessary. We will present at first methods, based for instance on canonical proofs or matrix characterizations, for proof construction in some LL fragments and their applications. Then, we will consider the notion of proof net that provides a nice, graphical representation of proofs (without some syntactical bureaucracy) and present new methods for automated proof nets construction in various fragments of LL. Relationship and comparisons between the both approaches will be discussed.
Type de document :
Communication dans un congrès
COST 15 LIEGE Seminar on Non Classical Logics for Computer Science Applications, invited lecture, 1998, Liege/Belgium, 1 p, 1998
Liste complète des métadonnées

https://hal.inria.fr/inria-00098600
Contributeur : Publications Loria <>
Soumis le : lundi 25 septembre 2006 - 17:03:53
Dernière modification le : mardi 24 avril 2018 - 13:34:43

Identifiants

  • HAL Id : inria-00098600, version 1

Collections

Citation

Didier Galmiche. Proof construction in linear logic and programming. COST 15 LIEGE Seminar on Non Classical Logics for Computer Science Applications, invited lecture, 1998, Liege/Belgium, 1 p, 1998. 〈inria-00098600〉

Partager

Métriques

Consultations de la notice

174