A Model-Driven Geometry Theorem Prover.
Shimon Ullman · Defense Technical Information Center (DTIC) · 1975
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.