On proof normalization in linear logic (Q1342248): Difference between revisions

Classical linear logic has been introduced by Girard as a logic of actions. Compared to classical logic, the two structural rules weakening and contraction are dropped from the Gentzen-type rules. In this system each resource (hypothesis) must be used exactly once. Classical linear logic is a very rich system. It is used for studying various aspects in computer science, for example concurrent aspects in logic programming, Petri nets reachability, just to name two of them. In this paper a proof-theoretic foundation for automated deduction in linear logic is presented. The main features investigated are the permutability properties of the inference rules. If two inferences in a proof can be exchanged without affecting the correctness of the proof, this means a redundancy in the search space. Efficient proof search procedures need to restrict the search space as much as possible, and elimination of redundancy is a very crucial aspect. Various permutability properties are investigated in the paper leading to the notion of a normalized proof. The precise criterion of a normalized proof given in the paper is quite complex, but the intuitive idea is to fix the position of the permutable inference steps in the proof. The results on proof normalization are not yet turned into a proof search strategy.