Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Guy Perrier Connect in order to contact the contributor
Submitted on : Monday, April 4, 2016 - 5:48:10 PM
Last modification on : Friday, February 4, 2022 - 3:12:11 AM
Long-term archiving on: : Monday, November 14, 2016 - 4:13:51 PM


Files produced by the author(s)


  • HAL Id : hal-01297758, version 1



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⟩



Record views


Files downloads