  The material presented in this paper contributes to establishing a basis
deemed essential for substantial progress in Automated Deduction. It identifies
and studies global features in selected problems and their proofs which offer
the potential of guiding proof search in a more direct way. The studied
problems are of the wide-spread form of "axiom(s) and rule(s) imply goal(s)".
The features include the well-known concept of lemmas. For their elaboration
both human and automated proofs of selected theorems are taken into a close
comparative consideration. The study at the same time accounts for a coherent
and comprehensive formal reconstruction of historical work by {\L}ukasiewicz,
Meredith and others. First experiments resulting from the study indicate novel
ways of lemma generation to supplement automated first-order provers of various
families, strengthening in particular their ability to find short proofs.
