Automated elementary geometry theorem discovery via inductive diagram manipulation

• Main Author: Johnson, Lars Erik
• Other Authors: Gerald Jay Sussman.
• Format: Others
• Language: English
• Published: Massachusetts Institute of Technology 2016
• Subjects: Electrical Engineering and Computer Science.
• Online Access: http://hdl.handle.net/1721.1/101450

Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2015. === This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections. === Cataloged from student-submitted PDF version of thesis. === Includes bibliographical references (pages 195-197). === I created and analyzed an interactive computer system capable of exploring geometry concepts through inductive investigation. My system begins with a limited set of knowledge about basic geometry and enables a user interacting with the system to teach the system additional geometry concepts and theorems by suggesting investigations the system should explore to see if it "notices anything interesting." The system uses random sampling and physical simulations to emulate the more humanlike processes of manipulating diagrams "in the mind's eye." It then uses symbolic pattern matching and a propagator-based truth maintenance system to appropriately generalize findings and propose newly discovered theorems. These theorems could be rigorously proved using external proof assistants, but are also used by the system to assist in its explorations of new, higher-level concepts. Through a series of simple investigations similar to an introductory course in geometry, the system has been able to propose and learn a few dozen standard geometry theorems. === by Lars Erik Johnson. === M. Eng.