 Therefore, in a theorem prover for many-sorted calculus there is no guarantee of getting an answer to the question: Does \(\Gamma \models \varphi\)? However, there are efficient theorem provers able to solve the problem in many cases; for instance, when there are decidable fragments to implement. See the entries on  automated reasoning  and  Church’s type theory.  Section 4 of the entry on Church’s type theory is devoted to automation and provides information about machine-oriented proof calculi as well as early proof assistants. An excellent selection of theorem provers for Church’s type theory are presented. Among them are LEO-II and LEO-III, the latter is said to “cooperate with first-order reasoning tools using translations to many-sorted logic”.