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

https://hal.inria.fr/hal-01297758
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

File

lfcs1994.pdf
Files produced by the author(s)

Identifiers

  • 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. pp.101-113. ⟨hal-01297758⟩

Share

Metrics

Record views

115

Files downloads

36