Formalization of Wu’s Simple Method in Coq

  • Jean-David Génevaux
  • Julien Narboux
  • Pascal Schreck
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7086)


We present in this paper the integration within the Coq proof assistant, of a method for automatic theorem proving in geometry. We use an approach based on the validation of a certificate. The certificate is generated by an implementation in Ocaml  of a simple version of Wu’s method.


formalization automation geometry Wu’s method proof assistant Coq 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BDG11]
    Boespflug, M., Dénès, M., Grégoire, B.: Full Reduction at Full Throttle. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 357–372. Springer, Heidelberg (2011)Google Scholar
  2. [CG90]
    Chou, S.-C., Gao, X.-S.: Ritt-Wu’s Decomposition Algorithm and Geometry Theorem Proving. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 207–220. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  3. [CG92]
    Chou, S.-C., Gao, X.-S.: A Class of Geometry Statements of Constructive Type and Geometry Theorem Proving. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 20–34. Springer, Heidelberg (1992)Google Scholar
  4. [CGZ94]
    Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994)CrossRefzbMATHGoogle Scholar
  5. [Cho88]
    Chou, S.-C.: Mechanical Geometry Theorem Proving. D. Reidel Publishing Company (1988)Google Scholar
  6. [Coq10]
    Coq development team. The Coq proof assistant reference manual, Version 8.3. LogiCal Project (2010)Google Scholar
  7. [CW07]
    Chaieb, A., Wenzel, M.: Context Aware Calculation and Deduction. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/CALCULEMUS 2007. LNCS (LNAI), vol. 4573, pp. 27–39. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  8. [FT11]
    Fuchs, L., Théry, L.: A Formalization of Grassmann-Cayley Algebra in Coq and its Application to Theorems Proving in Projective Geometry. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) ADG 2010. LNCS (LNAI), vol. 6877, pp. 51–67. Springer, Heidelberg (2011)Google Scholar
  9. [Gao00]
    Gao, X.-S.: Geometry expert, software package (2000)Google Scholar
  10. [GC98a]
    Gao, X.-S., Chou, S.-C.: Solving geometric constraint systems. I. A global propagation approach. Computer Aided Design 30(1), 47–54 (1998)CrossRefGoogle Scholar
  11. [GC98b]
    Gao, X.-S., Chou, S.-C.: Solving geometric constraint systems. II. A symbolic approach and decision of Rc-constructibility. Computer Aided Design 30(2), 115–122 (1998)CrossRefGoogle Scholar
  12. [GL02]
    Gao, X.-S., Lin, Q.: MMP/Geometer – A Software Package for Automated Geometric Reasoning. In: Winkler, F. (ed.) ADG 2002. LNCS (LNAI), vol. 2930, pp. 44–66. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  13. [GM05]
    Grégoire, B., Mahboubi, A.: Proving Equalities in a Commutative Ring Done Right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98–113. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  14. [GPT11]
    Grégoire, B., Pottier, L., Théry, L.: Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS (LNAI), vol. 6301, pp. 42–59. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  15. [Har07]
    Harrison, J.: Automating Elementary Number-Theoretic Proofs Using Gröbner Bases. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 51–66. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  16. [Har09]
    Harrison, J.: Without Loss of Generality. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 43–59. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  17. [JNQ10]
    Janičić, P., Narboux, J., Quaresma, P.: The Area Method: a Recapitulation. Journal of Automated Reasoning (2010)Google Scholar
  18. [JQ06]
    Janičić, P., Quaresma, P.: System Description: GCLCprover + Geothms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 145–150. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  19. [Kap86]
    Kapur, D.: Geometry Theorem Proving using Hilbert’s Nullstellensatz. In: SYMSAC 1986: Proceedings of the fifth ACM Symposium on Symbolic and Algebraic Computation, New York, NY, USA, pp. 202–208. ACM Press (1986)Google Scholar
  20. [Mah06]
    Mahboubi, A.: Contributions à la certification des calculs dans R: théorie, preuves, programmation. PhD thesis, Université de Nice Sophia-Antipolis (November 2006)Google Scholar
  21. [Nar04]
    Narboux, J.: A Decision Procedure for Geometry in Coq. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 225–240. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  22. [Nar07]
    Narboux, J.: A graphical user interface for formal proofs in geometry. J. Autom. Reasoning 39(2), 161–180 (2007)CrossRefzbMATHGoogle Scholar
  23. [PBN11]
    Pham, T.-M., Bertot, Y., Narboux, J.: A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry. In: Murgante, B., Gervasi, O., Iglesias, A., Taniar, D., Apduhan, B.O. (eds.) ICCSA 2011, Part IV. LNCS, vol. 6785, pp. 368–383. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  24. [Pha10]
    Pham, T.M.: An Additional Tool About the Orientation for Theorem Proving in the Coq Proof Assitant. In: Proceedings of Automated Deduction in Geometry, ADG 2010 (2010)Google Scholar
  25. [Pot08]
    Pottier, L.: Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics. In: Sutcliffe, G., Rudnicki, P., Schmidt, R., Konev, B., Schulz, S. (eds.) Knowledge Exchange: Automated Provers and Proof Assistants. CEUR Workshop Proceedings, Doha, Qatar p. 418 (2008)Google Scholar
  26. [Rob02]
    Robu, J.: Geometry Theorem Proving in the Frame of the Theorema Project. PhD thesis, Johannes Kepler Universitt, Linz (September 2002)Google Scholar
  27. [Wan89]
    Wang, D.: A new theorem discovered by computer prover. Journal of Geometry 36, 173–182 (1989), doi:10.1007/BF01231031MathSciNetCrossRefzbMATHGoogle Scholar
  28. [Wan01]
    Wang, D.: Elimination Method. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  29. [Wan02]
    Wang, D.: GEOTHER 1.1: Handling and Proving Geometric Theorems Automatically. In: Winkler, F. (ed.) ADG 2002. LNCS (LNAI), vol. 2930, pp. 194–215. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  30. [Wan04]
    Wang, D.: Elimination Practice. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  31. [Wu78]
    Wu, W.-T.: On the Decision Problem and the Mechanization of Theorem Proving in Elementary Geometry. Scientia Sinica 21, 157–179 (1978)MathSciNetGoogle Scholar
  32. [YCG11]
    Ye, Z., Chou, S.-C., Gao, X.-S.: An Introduction to Java Geometry Expert. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS, vol. 6301, pp. 189–195. Springer, Heidelberg (2011)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Jean-David Génevaux
    • 1
  • Julien Narboux
    • 1
  • Pascal Schreck
    • 1
  1. 1.LSIIT UMR 7005 CNRSUniversité de StrasbourgFrance

Personalised recommendations