Model-Driven Geometry Theorem Prover
Author(s)
Ullman, Shimon
DownloadAIM-321.ps (2.931Mb)
Additional downloads
Metadata
Show full item recordAbstract
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.
Date issued
1975-05-01Other identifiers
AIM-321
Series/Report no.
AIM-321