Abstract
In this paper a method for mechanical theorem proving in geometries is proposed. We first discuss how to describe geometric objects and geometric relations in 2D and/or 3D Euclidean space with Clifford algebraic expression. Then we present some rules to simplify Clifford algebraic polynomials to the so-called final Clifford algebraic polynomials. The key step for proving the theorems is to check if a Clifford algebraic expression can be simplified to zero. With the help of introducing coordinates, we can prove mechanically most of the geometric theorems about lines, conics, planes and so on in plane and/or solid geometry. The proofs produced by machine with our method are readable and geometrically interpretable. Finally, some interesting examples are given.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Machine proofs in geometry. World Scientific, Singapore (1995). 111, 128
Fèvre, S., Wang, D.: Proving geometric theorems using Clifford algebra and rewrite rules. In: Proc. CADE-15 (Lindau, Germany, July 5–10, 1998), LNAI 1421, pp. 17–32. 111
Boy de la Tour, T., Fèvre, S., Wang, D.: Clifford term rewriting for geometric reasoning in 3D. In this volume. 112
Hestenes, D., Sobczyk, G.: Clifford algebra to geometric calculus. D. Reidel, Dordrecht, Boston (1984). 112
Li, H.-B., Cheng, M.-t.: Proving theorems in elementary geometry with Clifford algebraic method. Chinese Math. Progress 26: 357–371 (1997). 111
Wu, W.-t.: Mechanical theorem proving in geometries: Basic principles. Springer, Wien New York (1994). 111
Yang, H.-Q.: Clifford algebra and mechanical theorem proving in geometries. Ph.D thesis, Jilin University, Changchun (1998). 120
Yang, H.-Q., Zhang, S.-G., Feng, G.-C.: Clifford algebra and mechanical geometry theorem proving. In: Proc. 3rd ASCM (Lanzhou, China, August 6–8, 1998), pp. 49–63. 114, 118, 124
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yang, H., Zhang, S., Feng, G. (1999). A Clifford Algebraic Method for Geometric Reasoning. In: Automated Deduction in Geometry. ADG 1998. Lecture Notes in Computer Science(), vol 1669. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47997-X_7
Download citation
DOI: https://doi.org/10.1007/3-540-47997-X_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66672-1
Online ISBN: 978-3-540-47997-0
eBook Packages: Springer Book Archive