The purpose of this study is to investigate a computational model for Euclidean geometry theorem proving with construction. “Construction” means drawing additional geometric elements in the problem figure. Some geometry theorems require construction as a part of the proof. The basic idea of our construction procedure is to add only elements required for applying a postulate that has a consequence that unifies with a goal to be proven. In other words, a construction is made only if it supports backward application of a postulate. Our major finding is that our proof procedure is semi-complete and useful in practice. In particular, an empirical evaluation showed that our theorem prover, GRAMY, solves all 17 construction problems from school textbooks as well as 86% (18 out of 21) of the construction problems solved by the preceding studies on automated geometry theorem proving. Three problems that GRAMY failed to solve require multiple constructions, and were solved by ad-hoc heuristics in the previous work.
For a PDF full article version, click here (281KB).