The paper presents sound and complete translations of several fragments of Martin-Löf's monomorphic type theory to first-order predicate calculus. The translations are optimized for the purpose of automated theorem proving in the mentioned fragments. The implementation of the theorem prover Gandalf and several experimental results are described.