A geometry theorem prover for macintoshes

Abstract

This geometry prover for Macintoshes is based on a prover developed on Symbolics Lisp Machines which is in turn based on the work by Wu [6] [7]. It can prove a subset of theorems that the original prover proved. It addresses a class of geometry statements called class C ([1] or [3]) and is complete for a subclass of class C, called class C_e [1]. It is powerful enough to prove many hard theorems such as Pappus' theorem, Simson's theorem, Pascal's theorem, the nine-point theorem, Feuerbach's theorem, Steiner's theorem, etc. With a further extension, it is expected to prove over 90% of the theorems that the original prover proved, including Morley's trisector theorem. this prover is mainly based on the method described in [1] or [3].

A disk of Mac plus or SE version can be obtained by writing to me. In the disk, there are a system fold, the program, a file (named “sample.lisp”) containing 12 sample examples, and a documentation [2] (serving as a kind of manual) in the T_EX file form. The disk can run on the mac plus and SE(SE/30) without using a hard disk.

The work reported here was supported in part by the NSF Grants CCR-9002362 and CCR-9117870