ON PROOF NORMALIZATION IN LINEAR LOGIC

We present a proof-theoretic foundation for automated deduction in lin ear logic. At first, we systematically study the permutability propert ies of the inference rules in this logic framework and exploit these t o introduce an appropriate notion of forward and backward movement of an inference in a proof. Then we discuss the naturally-arising questio n of the redundancy reduction and investigate the possibilities of pro of normalization which depend on the proof search strategy and the fra gment we consider. Thus, we can define the concept of normal proof tha t might be the basis of works about automatic proof construction and d esign of logic programming languages based on linear logic.