GRAMY: A Geometry Theorem Prover Capable of Construction
N. Matsuda, and K. VanLehn. Journal of Automated Reasoning, 32 (1):
3--33(January 2004)
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 -
%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
}