Proof strategies in linear logic (Q1340963)

Contraction and weakening are deduction rules that allow to use a hypothesis several times, once or never in a proof. Dealing with such rules is a major problem in automated theorem proving. Without these rules predicate calculus is decidable and simple algorithms can be designed. Linear logic is a refinement of classical logic that allows some control on contraction and weakening. Wide fragments of linear logic are decidable and their investigation has been recently a rather active field of research. In this paper, the author investigates and compares several proof search methods (bottom-up and top-down) for propositional and predicate linear logic. One of the issues of the paper is to get decision methods for some fragments of linear logic (e.g., without exponentials) but also to implement algorithms as efficient as possible: performances of the algorithms (in terms of time of execution and number of propositions generated) are analyzed on many examples and several optimizations of the naive algorithms are proposed.