%0 Journal Article %1 keyhere %A Matsuda, Noboru %A VanLehn, Kurt %D 2004 %J Journal of Automated Reasoning %K automated constraint construction control geometry intelligent problem proving satisfaction search system theorem tutoring %N 1 %P 3--33 %T GRAMY: A Geometry Theorem Prover Capable of Construction %U http://dx.doi.org/10.1023/B:JARS.0000021960.39761.b7 %V 32 %X This study investigates a procedure for proving arithmetic-free Euclidean geometry theorems that involve 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, 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 arithmetic-free construction problems from a sample of school textbooks and 86% of the arithmetic-free construction problems solved by preceding studies of automated geometry theorem proving. ER -

@article{keyhere, abstract = {This study investigates a procedure for proving arithmetic-free Euclidean geometry theorems that involve 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, 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 arithmetic-free construction problems from a sample of school textbooks and 86% of the arithmetic-free construction problems solved by preceding studies of automated geometry theorem proving. ER -}, added-at = {2008-05-22T14:06:35.000+0200}, author = {Matsuda, Noboru and VanLehn, Kurt}, biburl = {https://www.bibsonomy.org/bibtex/2efa5c4f78574825e5429500aa668287d/toni}, description = {SpringerLink - Journal Article}, interhash = {eb8d319e2f9997925998a9ecbce8b553}, intrahash = {efa5c4f78574825e5429500aa668287d}, journal = {Journal of Automated Reasoning}, keywords = {automated constraint construction control geometry intelligent problem proving satisfaction search system theorem tutoring}, month = {#jan#}, number = 1, pages = {3--33}, timestamp = {2008-06-05T14:36:10.000+0200}, title = {GRAMY: A Geometry Theorem Prover Capable of Construction}, url = {http://dx.doi.org/10.1023/B:JARS.0000021960.39761.b7}, volume = 32, year = 2004 }