A procedure for automatic proof nets construction

Didier Galmiche 1, 2 Guy Perrier 2, 1
2 Prograis
INRIA Lorraine, CRIN - Centre de Recherche en Informatique de Nancy
Abstract : In this paper, we consider multiplicative linear logic (MLL) from an automated deduction point of view. Linear logic is more expressive than classical and intuitionistic logic and has an undirectional character due to the particular treatment of negation and the absence of structural rules. Considering this new logical framework to make logic programming or programming with proofs (extracting programs from proofs), a better comprehension of proofs in MLL (proof nets) is necessary and automated deduction has to be studied. Knowing that the multiplicative part of linear logic is decidable, we propose a new algorithm to construct automatically a proof net for a given sequent in MLL with proofs of termination, correctness and completeness. It can be considered as a more direct and implementation oriented way to consider automated deduction in linear logic.
Type de document :
Communication dans un congrès
Conference on Logic Programming and Automated Reasoning, LPAR'92, 1992, St-Petersburg, Russia. 624, pp.42-53, 1992, LNCS
Liste complète des métadonnées

https://hal.inria.fr/hal-01297750
Contributeur : Guy Perrier <>
Soumis le : lundi 4 avril 2016 - 17:37:08
Dernière modification le : jeudi 11 janvier 2018 - 06:28:03
Document(s) archivé(s) le : lundi 14 novembre 2016 - 16:03:43

Fichier

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

Identifiants

  • HAL Id : hal-01297750, version 1

Collections

Citation

Didier Galmiche, Guy Perrier. A procedure for automatic proof nets construction. Conference on Logic Programming and Automated Reasoning, LPAR'92, 1992, St-Petersburg, Russia. 624, pp.42-53, 1992, LNCS. 〈hal-01297750〉

Partager

Métriques

Consultations de la notice

140

Téléchargements de fichiers

34