Proving geometric theorems using clifford algebra and rewrite rules
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 effectively in this coordinate-free manner. This paper describes the method in detail and reports on our preliminary experiments.
Unable to display preview. Download preview PDF.
- 2.Balbiani, P., Fariñas del Cerro, L.: Affine geometry of collinearity and conditional term rewriting. In: Proc. French Spring School Theor. Comput. Sci. (Font-romeu, May 17–21, 1993), LNCS 909, pp. 196–213 (1995).Google Scholar
- 5.Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated geometry theorem proving by vector calculation. In: Proc. ISSAC '93 (Kiev, July 6–8, 1993), pp. 284–291.Google Scholar
- 7.Contejean, E., Marché, C., Rabehasaina, L.: Rewrite systems for natural, integral and rational arithmetic. Technical report, L.R.I., Université de Paris-Sud, France (1997).Google Scholar
- 8.Fèvre, S.: Integration of reasoning and algebraic calculus in geometry. In: Automated deduction in geometry (D. Wang et al., eds.), LNAI 1360, pp. 218–234 (1998).Google Scholar
- 12.Kapur, D., Saxena, T., Yang, L.: Algebraic and geometric reasoning using Dixon resultants. In: Proc. ISSAC '94 (Oxford, July 20–22, 1994), pp. 99–107.Google Scholar
- 14.Li, H.: New explorations on mechanical theorem proving of geometries. Ph.D thesis, Beijing University, China (1994).Google Scholar
- 18.Stifter, S.: Geometry theorem proving in vector spaces by means of Gröbner bases. In: Proc. ISSAC '93 (Kiev, July 6–8, 1993), pp. 301–310.Google Scholar
- 20.Wang, D.: Clifford algebraic calculus for geometric reasoning with application to computer vision. In: Automated deduction in geometry (D. Wang et al., eds.), LNAI 1360, pp. 115–140 (1998).Google Scholar
- 21.Wu, W.-t.: Basic principles of mechanical theorem proving in elementary geometries. J. Syst. Sci. Math. Sci. 4: 207–235 (1984).Google Scholar