A Model-Driven Geometry Theorem Prover.
Abstract
This paper describes a new Geometry Theorem Prover, which was implemented to illuminate some issues related to the use of models in theorem proving. The paper is divided into three parts: Part 1 describes the G.T.P. and presents the ideas embedded in it. Part 2 describes the backward search mechanism. Part 3 addresses the notion of similarity in a problem, defines a notion of semantic symmetry, and compares it to Gelernter's concept of syntactic symmetry.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 1975
- Accession Number
- ADA021446
Entities
People
- Shimon Ullman
Organizations
- Massachusetts Institute of Technology