Foundations of Proof Search Strategies Design in Linear Logic

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 investigate automated proof construction in classical linear logic (CLL) by giving logical foundations for the design of proof search strategies. We propose common theoretical foundations for top-down, bottom-up and mixed proof search procedures with a systematic formalization of strategies construction using the notions of {\em immediate or chaining composition or decomposition}, deduced from permutability pro\-perties and inference movements in a proof. Thus, we have logical bases for the design of proof strategies in CLL fragments and then we can propose sketches for their design.
Type de document :
Communication dans un congrès
Logical Foundations of Computer Science, 1994, St-Petersburg, Russia. 813, pp.101-113, LNCS
Liste complète des métadonnées

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

Fichier

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

Identifiants

  • HAL Id : hal-01297758, version 1

Collections

Citation

Didier Galmiche, Guy Perrier. Foundations of Proof Search Strategies Design in Linear Logic. Logical Foundations of Computer Science, 1994, St-Petersburg, Russia. 813, pp.101-113, LNCS. 〈hal-01297758〉

Partager

Métriques

Consultations de la notice

161

Téléchargements de fichiers

35