{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/101450"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/101450","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Automated elementary geometry theorem discovery via inductive diagram manipulation","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Johnson, Lars Erik"],"institution":"Massachusetts Institute of Technology","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science.","school":null,"contributors":[],"advisors":["Gerald Jay Sussman."],"committee_chairs":[],"committee_members":[],"year":2015,"date_issued":"2015","date_published":"2015","updated_at":"2026-07-22T22:22:20Z","subjects":["Electrical Engineering and Computer Science."],"languages":["eng"],"rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/1721.1/101450","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Gerald Jay Sussman."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."]},{"key":"dc:creator","label":"Author","values":["Johnson, Lars Erik"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2016-03-03T20:29:20Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2016-03-03T20:29:20Z"]},{"key":"dc:date.issued","label":"Date","values":["2015"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Electrical Engineering and Computer Science."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/1721.1/101450"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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)."]},{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["M. Eng."]},{"key":"dc:title","label":"Title","values":["Automated elementary geometry theorem discovery via inductive diagram manipulation"]}]}],"canonical_facts":{"dc:contributor.advisor":["Gerald Jay Sussman."],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:contributor.other":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:creator":["Johnson, Lars Erik"],"dc:date.accessioned":["2016-03-03T20:29:20Z"],"dc:date.available":["2016-03-03T20:29:20Z"],"dc:date.issued":["2015"],"dc:description":["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)."],"dc:description.abstract":["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."],"dc:description.degree":["M. Eng."],"dc:identifier.uri":["http://hdl.handle.net/1721.1/101450"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Electrical Engineering and Computer Science."],"dc:title":["Automated elementary geometry theorem discovery via inductive diagram manipulation"],"dc:type":["Thesis"]},"updated_at":"2026-07-22T22:22:20Z"}