The representation of a proof as you find it in textbooks is just a linear sequence of derivation steps. This does not mean that linear sequences of derivation steps are a good representation for computer generated and computer manipulated proofs. And in fact, for various calculi there are alternative and more compact representations of proofs, for example Shostak's refutation graphs for resolution proofs in predicate logic, or Girard's proof nets in linear logic. One of the features of these proof representations is that they abstract from irrelevant orderings of derivation steps. They are therefore a representation for a whole class of proofs. In the paper the idea of proof nets for linear logic is adapted to the non-commutative Lambek calculus. Based on this kind of proof nets as data structures, new algorithms for automatic theorem proving are presented which can exploit a fair degree of parallelism.