Foundations of Proof Search Strategies Design in Linear Logic

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.