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 <>
Submitted on : Monday, April 4, 2016 - 5:48:10 PM
Last modification on : Wednesday, May 12, 2021 - 4:56:04 PM
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