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.
https://hal.inria.fr/hal-01297758
Contributeur : Guy Perrier
<>
Soumis le : lundi 4 avril 2016 - 17:48:10
Dernière modification le : jeudi 11 janvier 2018 - 06:28:03
Document(s) archivé(s) le : lundi 14 novembre 2016 - 16:13:51
Didier Galmiche, Guy Perrier. Foundations of Proof Search Strategies Design in Linear Logic. Logical Foundations of Computer Science, 1994, St-Petersburg, Russia. 813, pp.101-113, LNCS. 〈hal-01297758〉
