Combining Clifford Algebraic Computing and Term-Rewriting for Geometric Theorem Proving

Article type: Research Article

Authors: Fèvre, Stéphane | Wang, Dongming

Affiliations: Laboratoire LEIBNIZ – Institut IMAG, 46, avenue Félix Viallet, 38031 Grenoble Cedex, France. {Stephane.Fevre,Dongming.Wang}@imag.fr

Note: [] Address for correspondence: Laboratoire LEIBNIZ - Institut IMAG, 46 avenue Félix Viallet, 38031 Grenoble Cedex, France

Abstract: A general approach we have proposed for automatically proving geometric theorems requires both Clifford algebraic reduction and term-rewriting. This paper shows how efficient techniques and software tools developed in the areas of algebraic computation and term-rewriting can be combined for our purpose of theorem proving in geometry. Some investigations and experiments for concrete cases have been carried out by combining routines implemented in Maple V and Objective Caml. The experiments together with several examples illustrate the suitability and performance of our approach.

Keywords: System combination, algebraic computing, term-rewriting, Clifford algebra, geometric theorem proving

DOI: 10.3233/FI-1999-391205

Journal: Fundamenta Informaticae, vol. 39, no. 1-2, pp. 85-104, 1999