This paper first introduces the theory and algorithm of mating method in automatic theorem proving advanced by Peter B. Andrews, and then gives an implementation algorithm without backtracking, finally obtains a theorem proving system for higher order logic.