Abstract
The existing readable machine proving methods deal with geometry problems using some geometric quantities. In this paper, we focus on the mass point method which directly deals with the geometric points rather than the geometric quantities. We propose two algorithms, Mass Point Method and Complex Mass Point Method, which can deal with the Hilbert intersection point statements in affine geometry and the linear constructive geometry statements in metric geometry respectively. The two algorithms are implemented in Maple as provers. The results of hundreds of non-trivial geometry statements run by our provers show that the mass point method is efficient and the machine proofs are human-readable.
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
Zhang, J.Z., Li, Y.B.: Automaic theorem proving for three decades. Journal of Systems Science and Mathematical Sciences (J. Sys. Sci. & Math. Scis.) 29, 1155–1168 (2009)
Wu, W.T.: On the Decision Problem and The Mechanization of Theorem Proving in Elemengtary Geometry. In: Automated Theorem Proving: After 25 years, vol. 29, pp. 213–214. American Mathematical Society (1984)
Chou, S.C.: Proving and dicoversing geometry theorems using Wu’s method. Ph.D. thsis. The University of Texas, Austin (1985)
Wang, D.: Reasoning about geometric problems using an elimination method. In: Pfalzgraf, J., Wang, D. (eds.) Automated Practical Reasoning, pp. 147–185. Springer, New York (1995)
Kapur, D.: Using Gröbner bases to reason about geometry problems. Journal of Symbolic Computation 2, 399–408 (1986)
Chou, S.C.: Automated reasoning in geometries using the characteristic set method and Gröbner basis method. In: Proc. ISSAC 1990, Tokyo, pp. 255–260 (1990)
Li, H.: Clifford algebra approaches to mechanical geometry theorem proving. In: Gao, X.S., Wang, D. (eds.) Mathematics Mechanization and Applications, pp. 205–299. Academic Press, San Diego (2000)
Hong, J.: Can we prove geometry theorems by computing an example? Sci. Sinica. 29, 824–834 (1986)
Yang, L., Zhang, J.Z., Li, C.Z.: A prover for parallel numerical verification of a class of constructive geometry theorems. In: Proc. IWMM 1992, pp. 244–255. Inter. Academic Publishers, Beijing (1992)
Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated production of traditional proofs for constructive geometry theorems. In: Vardi, M. (ed.) Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science LICS, Montreal, pp. 48–56 (1993)
Chou, S.C., Gao, X.S., Zhang, J.Z.: Machine proofs in geometry: Automated production of readable proofs for geometry theorems. World Scientific, Singapore (1994)
Chou, S.C., Gao, X.S., Zhang, J.Z.: A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning 25, 219–246 (1996)
Chou, S.C., Gao, X.S., Zhang, J.Z.: Mechanical theorem proving by vector calculation. In: Proc ISSAC 1993, Keiv, pp. 284–291 (1993)
Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated production of readable proofs with geometric invariants, theorem proving with full-angles. Journal of Automated Reasoning 17, 349–370 (1996)
Li, H., Hestenes, D.: Rockwood A. Generalized homogeneous coordinates for computational geometry. In: Sommer, G. (ed.) Geometric Computing with Clifford Algebra, pp. 27–60. Springer, Heidelberg (2000)
Li, H.: Automated Geometric Theorem Proving, Clifford bracket algebra and Clifford expansions. In: Trends in Mathematics: Advances in Analysis and Geometry, pp. 345–363. Birkhäuser, Basel (2004)
Li, H.: Symbolic computation in the homogeneous geometric model with Clifford algebra. In: Gutierrez, J. (ed.) Proc. ISSAC 2004, pp. 221–228. ACM Press (2004)
Li, H.: Invariant algebras and geometric reasoning. World Scientific, Singapore (2008)
Rhoad, R., Milauskas, G., Whipple, R.: Geometry for Enjoyment and Challenge. McDougal, Littell & Company (1991)
Pedoe, D.: Notes on the History of Geometrical Ideas I: Homogeneous Coordinates. Math. Magazine, 215–217 (1975)
Tom, R.: Mass point geometry, http://mathcircle.berkeley.edu/archivedocs/2007_2008/lectures/0708lecturesps/MassPointsBMC07.ps
Tom, R.: Mass point geometry (Barycentirc Coordinates), http://mathcircle.berkeley.edu/archivedocs/1999_2000/lectures/9900lecturespdf/mpgeo.pdf
Coxeter, H.S.M.: Introduction to Geometry, pp. 216–221. John Wiley & Sons, Inc. (1969)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zou, Y., Zhang, J. (2011). Automated Generation of Readable Proofs for Constructive Geometry Statements with the Mass Point Method. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds) Automated Deduction in Geometry. ADG 2010. Lecture Notes in Computer Science(), vol 6877. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25070-5_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-25070-5_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25069-9
Online ISBN: 978-3-642-25070-5
eBook Packages: Computer ScienceComputer Science (R0)