Automated theorem proving in linear logic Is automatic theorem proving and proof searching easier in linear and other propositional substructural logics which lack contraction? 

Where can I read more about automatic theorem proving in these logics and the role of contraction in proof search?
Other resources could be found referenced in Kaustuv Chaudhuri's thesis "The Focused Inverse Method for Linear Logic", and you might be interested in Roy Dyckhoff's "Contraction-Free Sequent Calculi", which is about contraction but not about linear logic.

There are opportunities for efficient proof search in linear logic, but I don't think current work indicates that it's easier than proof search in non-substructural logic. The problem is that if you want to prove $C \vdash(A \otimes B)$ in linear logic, you have an extra question that you don't have in normal proof search: is $C$ used to prove $A$ or is $C$ used to prove $B$? In practice, this "resource nondeterminism" is a big problem in performing proof search in linear logic.

Per the comments, Lincoln et al's 1990 "Decision problems for propositional linear logic" is a good reference if you want to get technical about words like "easier."