Everyday Reasoning Meets Geometry Theorem-Proving

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 12

Student Abstracts

In an earlier paper [McDougal and Hammond 1993], we reported on POLYA, a computer program which proves high school geometry theorems. POLYA is a memory-based problem-solver in the case-based planning tradition [Hammond 1989, Kolodner 1993]. It uses features of the problem (mostly from the diagram) to index into a library of plans. Some of those plans are solutions to entire problems; others apply a single inference. The plans are indexed in memory by the features which predict the relevance of the plan without necessarily guaranteeing it.