Name
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. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1023/B:JARS.0000021960.39761.b7 | J. Autom. Reasoning |
Keywords | Field | DocType |
automated geometry theorem proving,construction,search control,constraint satisfaction problem,intelligent tutoring system | Discrete mathematics,Intelligent tutoring system,Automated theorem proving,Constraint satisfaction problem,If and only if,Euclidean geometry,Geometry,Proof procedure,Mathematics | Journal |
Volume | Issue | ISSN |
32 | 1 | 1573-0670 |
Citations | PageRank | References |
18 | 1.50 | 11 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Noboru Matsuda | 1 | 200 | 23.45 |
| Kurt VanLehn | 2 | 2352 | 417.44 |