This paper presents an algorithm for proving plane geometry theorems stated by text and diagram in a complementary way. The problem of proving plane geometry theorems involves two challenging subtasks, being theorem understanding and theorem proving. This paper proposes to consider theorem understanding as a problem of extracting relations from text and diagram. A syntax-semantics (S2) model method is proposed to extract the geometric relations from theorem text, and a diagram mining method is proposed to extract geometry relations from diagram...
