 The development, respectively improvement, of machine-oriented proof calculi for Church’s type theory is still a challenge research topic. Compared, e.g., to the theoretical and practical maturity achieved in first-order automated theorem proving, the area is still in its infancy. Obviously, the challenges are also much bigger than in first-order logic. The practically way more expressive nature of the term-language of Church’s type theory causes a larger, bushier and more difficult to traverse proof search space than in first-order logic. Moreover, remember that unification, which constitutes a very important control and filter mechanism in first-order theorem proving, is undecidable (in general) in type theory; see  Section 3.2.  On the positive side, however, there is a chance to find significantly shorter proofs than in first-order logic. This is well illustrated with a small, concrete example in Boolos 1987. Clearly, much further progress is needed to further leverage the practical relevance of existing calculi for Church’s type theory and their implementations (see  Section 4.3).  The challenges include