Advertisement

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)

Abstract

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.

Keywords

formalization automation geometry Wu’s method proof assistant Coq 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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