GRAMY: A geometry theorem prover capable of construction

Noboru Matsuda, Kurt Vanlehn

Research output: Contribution to journalArticlepeer-review

30 Scopus citations


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 languageEnglish (US)
Pages (from-to)3-33
Number of pages31
JournalJournal of Automated Reasoning
Issue number1
StatePublished - 2004
Externally publishedYes


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

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence


Dive into the research topics of 'GRAMY: A geometry theorem prover capable of construction'. Together they form a unique fingerprint.

Cite this