Automated elementary geometry theorem discovery via inductive diagram manipulation
Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2015.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2016
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/101450 |
| _version_ | 1826214682549026816 |
|---|---|
| author | Johnson, Lars Erik |
| author2 | Gerald Jay Sussman. |
| author_facet | Gerald Jay Sussman. Johnson, Lars Erik |
| author_sort | Johnson, Lars Erik |
| collection | MIT |
| description | Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2015. |
| first_indexed | 2024-09-23T16:09:22Z |
| format | Thesis |
| id | mit-1721.1/101450 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T16:09:22Z |
| publishDate | 2016 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/1014502019-04-12T12:06:04Z Automated elementary geometry theorem discovery via inductive diagram manipulation Johnson, Lars Erik Gerald Jay Sussman. Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science. Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science. Electrical Engineering and Computer Science. 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. 2016-03-03T20:29:20Z 2016-03-03T20:29:20Z 2015 2015 Thesis http://hdl.handle.net/1721.1/101450 939918000 eng 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. http://dspace.mit.edu/handle/1721.1/7582 197 pages application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Johnson, Lars Erik Automated elementary geometry theorem discovery via inductive diagram manipulation |
| title | Automated elementary geometry theorem discovery via inductive diagram manipulation |
| title_full | Automated elementary geometry theorem discovery via inductive diagram manipulation |
| title_fullStr | Automated elementary geometry theorem discovery via inductive diagram manipulation |
| title_full_unstemmed | Automated elementary geometry theorem discovery via inductive diagram manipulation |
| title_short | Automated elementary geometry theorem discovery via inductive diagram manipulation |
| title_sort | automated elementary geometry theorem discovery via inductive diagram manipulation |
| topic | Electrical Engineering and Computer Science. |
| url | http://hdl.handle.net/1721.1/101450 |
| work_keys_str_mv | AT johnsonlarserik automatedelementarygeometrytheoremdiscoveryviainductivediagrammanipulation |