In order to fully tap the educational value of geometry theorem proving theory and meet the actual needs of geometry teaching in secondary school, this project focuses on the so-called restricted automated geometry theorem proving. The aim of our research is not only to improve the ability and efficiency of the proving algorithm, but also to place some limit on the rules in proving, the length of proof procedure and the proof expression style to meet the teaching needs. The outcome of this project will provide a solid foundation for the development of intelligent educational software in math.