## 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.

Original language | English (US) |
---|---|

Pages (from-to) | 3-33 |

Number of pages | 31 |

Journal | Journal of Automated Reasoning |

Volume | 32 |

Issue number | 1 |

DOIs | |

State | Published - 2004 |

Externally published | Yes |

## Keywords

- Automated geometry theorem proving
- Constraint satisfaction problem
- Construction
- Intelligent tutoring system
- Search control

## ASJC Scopus subject areas

- Software
- Computational Theory and Mathematics
- Artificial Intelligence