Foundations of Proof Search Strategies Design in Linear Logic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 1994

Foundations of Proof Search Strategies Design in Linear Logic

Guy Perrier
  • Fonction : Auteur
  • PersonId : 8101
  • IdHAL : guy-perrier

Résumé

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.

Mots clés

Fichier principal
Vignette du fichier
lfcs1994.pdf (9.91 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-01297758 , version 1 (04-04-2016)

Identifiants

  • HAL Id : hal-01297758 , version 1

Citer

Didier Galmiche, Guy Perrier. Foundations of Proof Search Strategies Design in Linear Logic. Logical Foundations of Computer Science, 1994, St-Petersburg, Russia. pp.101-113. ⟨hal-01297758⟩
121 Consultations
42 Téléchargements

Partager

Gmail Facebook X LinkedIn More