Solving Geometry Problems using a
Combination of Symbolic and Numerical
We describe a framework that combines deductive, numeric,
and inductive reasoning to solve geometric problems. Applications include
the generation of geometric models and animations, as well as
problem solving in the context of intelligent tutoring systems.
Our novel methodology uses (i) deductive reasoning to generate a partial
program from logical constraints, (ii) numerical methods to evaluate
the partial program, thus creating geometric models which are solutions
to the original problem, and (iii) inductive synthesis to read off
new constraints that are then applied to one more round of deductive reasoning
leading to the desired deterministic program. By the combination of
methods we were able to solve problems that each of the methods was
not able to solve by itself.
The number of nondeterministic choices in a partial program provides a
measure of how close a problem is to being solved and can thus be used
in the educational context for grading and providing hints.
We have successfully evaluated our methodology on 18 Scholastic Aptitude
Test geometry problems, and 11 ruler/compass-based geometry
construction problems. Our tool solved these problems using an average
of a few seconds per problem.