Model-Driven Geometry Theorem Prover
This paper describes a new Geometry Theorem Prover, which was implemented to illuminate some issues related to the use of models in theorem provin. The paper is divided into three parts: Part 1 describes G.T.P. and presents the ideas embedded in it. It concentrates on the forward search method...
| Main Author: | |
|---|---|
| Language: | en_US |
| Published: |
2004
|
| Online Access: | http://hdl.handle.net/1721.1/5785 |
| _version_ | 1826188877158678528 |
|---|---|
| author | Ullman, Shimon |
| author_facet | Ullman, Shimon |
| author_sort | Ullman, Shimon |
| collection | MIT |
| description | This paper describes a new Geometry Theorem Prover, which was implemented to illuminate some issues related to the use of models in theorem provin. The paper is divided into three parts: Part 1 describes G.T.P. and presents the ideas embedded in it. It concentrates on the forward search method, and gives two examples of proofs produced that way. Part 2 describes the backward search mechanism and presents proofs to a sequence of successively harder problems. The last section of the work addresses the notion of similarity in a problem, defines a notion of semantic symmetry, and compares it to Gelernter's concept of syntactic symmetry. |
| first_indexed | 2024-09-23T08:06:04Z |
| id | mit-1721.1/5785 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T08:06:04Z |
| publishDate | 2004 |
| record_format | dspace |
| spelling | mit-1721.1/57852019-04-09T16:39:18Z Model-Driven Geometry Theorem Prover Ullman, Shimon This paper describes a new Geometry Theorem Prover, which was implemented to illuminate some issues related to the use of models in theorem provin. The paper is divided into three parts: Part 1 describes G.T.P. and presents the ideas embedded in it. It concentrates on the forward search method, and gives two examples of proofs produced that way. Part 2 describes the backward search mechanism and presents proofs to a sequence of successively harder problems. The last section of the work addresses the notion of similarity in a problem, defines a notion of semantic symmetry, and compares it to Gelernter's concept of syntactic symmetry. 2004-10-01T20:36:53Z 2004-10-01T20:36:53Z 1975-05-01 AIM-321 http://hdl.handle.net/1721.1/5785 en_US AIM-321 56 p. 3074279 bytes 2316645 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Ullman, Shimon Model-Driven Geometry Theorem Prover |
| title | Model-Driven Geometry Theorem Prover |
| title_full | Model-Driven Geometry Theorem Prover |
| title_fullStr | Model-Driven Geometry Theorem Prover |
| title_full_unstemmed | Model-Driven Geometry Theorem Prover |
| title_short | Model-Driven Geometry Theorem Prover |
| title_sort | model driven geometry theorem prover |
| url | http://hdl.handle.net/1721.1/5785 |
| work_keys_str_mv | AT ullmanshimon modeldrivengeometrytheoremprover |