We consider geometric theorems that can be stated constructively by introducing points, while each newly introduced point may be represented in terms of the previously constructed points using Clifford algebraic operators. To prove a concrete theorem, one first substitutes the expressions of the dependent points into the conclusion Clifford polynomial to obtain an expression that involves only the free points and parameters. A term-rewriting system is developed that can simplify such an expression to 0, and thus prove the theorem. A large class of theorems can be proved effctively in this coordinate-free manner. THis paper describes the method in detail and reports on our preliminary experiments.
展开▼
