On Proof Normalization in Linear Logic

Didier Galmiche 1, 2 Guy Perrier 2, 1
2 Prograis
INRIA Lorraine, CRIN - Centre de Recherche en Informatique de Nancy
Abstract : We present a proof-theoretic foundation for automated deduction in linear logic. At first, we systematically study the permutability properties of the inference rules in this logical framework and exploit these to introduce an appropriate notion of forward and backward movement of an inference in a proof. Then we discuss the naturally-arising question of the redundancy reduction and investigate the definition of the normal proof concept. We briefly consider some of the issues related to proof construction mechanization in linear logic and to the design of logic programming languages from linear logic fragments.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 1994, 135 (1), pp.67-110
Liste complète des métadonnées

https://hal.inria.fr/hal-01297755
Contributeur : Guy Perrier <>
Soumis le : lundi 4 avril 2016 - 17:42:32
Dernière modification le : jeudi 17 mai 2018 - 12:52:03
Document(s) archivé(s) le : lundi 14 novembre 2016 - 15:59:00

Fichier

tcs1994.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01297755, version 1

Collections

Citation

Didier Galmiche, Guy Perrier. On Proof Normalization in Linear Logic. Theoretical Computer Science, Elsevier, 1994, 135 (1), pp.67-110. 〈hal-01297755〉

Partager

Métriques

Consultations de la notice

252

Téléchargements de fichiers

52