AUTOMATIC THEOREM PROVING BASED ON MATINGS
基于配对方法的自动定理证明

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.