Skip to main content
SpringerLink
Log in

Formalization of Symplectic Geometry in HOL-Light

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11232))

Included in the following conference series:

Abstract

Symplectic geometry is a versatile geometric theory widely used in many disciplines such as analytical mechanics, geometric topology and Lie group. However, when symplectic geometry is applied in practice, the satisfaction of its preconditions is often not formally verified. Therefore, it is necessary to make verifications on symplectic geometry and its applications. The purpose of the present work is to conduct such verifications by establishing a formal theorem library in HOL-Light. For this purpose, seven basic concepts are formalized at first. Then, the properties of symplectic vector spaces and symplectic matrices are formally verified. To validate the correctness of the formalized symplectic geometry and to demonstrate its applications, formal analysis is finally made on the symplectic features of matrix optics. The present work not only lays a necessary foundation for formal verifications in this field but also extends the library of theories of the HOL-Light system. Based on this foundation, some more sophisticated symplectic geometry theories and their engineering applications can be further formalized and verified.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Antoñana, M., Makazaga, J., Murua, A.: Reducing and monitoring round-off error propagation for symplectic implicit Runge-Kutta schemes. Numer. Algorithms 76(4), 861–880 (2017). https://doi.org/10.1007/s11075-017-0287-z. ISSN: 1572-9265

    Article  MathSciNet  MATH  Google Scholar 

  2. Besana, A., Spera, M.: On some symplectic aspects of knot framings. J. Knot Theory Ramifications 15(07), 883–912 (2006)

    Article  MathSciNet  Google Scholar 

  3. Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 12–27. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24364-6_2

    Chapter  Google Scholar 

  4. Calvaruso, G., Ovando, G.P.: From almost (para)-complex structures to affine structures on lie groups. Manuscripta Math. 155, 89–113 (2016)

    Article  MathSciNet  Google Scholar 

  5. Frejlich, P., Torres, D.M., Miranda, E.: A note on the symplectic topology of b-manifolds. J. Symplectic Geom. 15, 719–739 (2017)

    Article  MathSciNet  Google Scholar 

  6. Gottliebsen, H., Hardy, R., Lightfoot, O., Martin, U.: Applications of real number theorem proving in PVS. Formal Aspects Comput. 25(6), 993–1016 (2013)

    Article  MathSciNet  Google Scholar 

  7. Guo, X.L., Dutta, R.G., Mishra, P., Jin, Y.E.: Automatic code converter enhanced PCH framework for SoC trust verification. IEEE Trans. Very Large Scale Integr. Syst. 25(12), 3390–3400 (2017)

    Article  Google Scholar 

  8. Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_4

    Chapter  Google Scholar 

  9. Hunt, J.W., Kaufmann, M., Moore, J.S., Slobodova, A.: Industrial hardware and software verification with ACL2. Philos. Trans. 375(2104), 20150399 (2017)

    Article  Google Scholar 

  10. Jeannin, J.B., et al.: A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. Int. J. Softw. Tools Technol. Transf. 230(1), 1–25 (2015)

    Google Scholar 

  11. Karshon, Y., Ziltener, F.: Hamiltonian group actions on exact symplectic manifolds with proper momentum maps are standard. Trans. Am. Math. Soc. 370, 1409–1425 (2016)

    Article  MathSciNet  Google Scholar 

  12. Li, Y., Sun, M.: Modeling and verification of component connectors in Coq, vol. 113. Elsevier North-Holland, Inc. (2015)

    Google Scholar 

  13. Ma, S., Shi, Z.P., Shao, Z.Z., Guan, Y., Li, L.M., Li, Y.D.: Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm. Adv. Appl. Clifford Algebras 26(4), 1305–1330 (2016)

    Article  MathSciNet  Google Scholar 

  14. Mei, L.J., Wu, X.Y.: Symplectic exponential Runge Kutta methods for solving nonlinear Hamiltonian systems. J. Comput. Phys. 338, 567–584 (2017)

    Article  MathSciNet  Google Scholar 

  15. Monteiro, F., Cordeiro, L., Filho, E.: ESBMC-GPU: a context-bounded model checking tool to verify CUDA programs. Sci. Comput. Program. 152(1), 63–69 (2017)

    Google Scholar 

  16. Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_6

    Chapter  Google Scholar 

  17. Tang, W., Zhang, J.: Symplecticity-preserving continuous-stage Runge Kutta nystr\(\ddot{o}\)m methods. Appl. Math. Comput. 323, 204–219 (2018)

    MathSciNet  Google Scholar 

  18. Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50(2), 229–241 (2013)

    Article  MathSciNet  Google Scholar 

  19. Wei, Q.X., Jiao, J., Zhao, T.D.: Flight control system failure modeling and verification based on spin. Eng. Fail. Anal. 82(1), 501–513 (2017)

    Article  Google Scholar 

  20. Zhao, C.N., Shi, L.K., Guan, Y., Li, X.J., Shi, Z.P.: Formal modeling and verification of fractional order linear systems. ISA Trans. 62, 87–93 (2016)

    Article  Google Scholar 

  21. Zhao, C.N., Li, S.S.: Formalization of fractional order PD control systems in HOL4. Theoret. Comput. Sci. 706(1), 22–34 (2017)

    MathSciNet  MATH  Google Scholar 

  22. Zheng, X., Julien, C., Kim, M., Khurshid, S.: Perceptions on the state of the art in verification and validation in cyber-physical systems. IEEE Syst. J. PP(99), 1–14 (2015)

    Google Scholar 

Download references

Acknowledgment

This work was supported by the National Natural Science Foundation of China (61472468, 61572331, 61602325, 61702348), the National Key Technology Research and Development Program (2015BAF13B01), National Key R&D Plan (2017YFC0806700, 2017YFB130253), the Project of the Beijing Municipal Science & Technology Commission (LJ201607) and Capital Normal University Major (key) Nurturing Project.

Author information

Authors and Affiliations

  1. Beijing Advanced Innovation Center for Imaging Technology, Capital Normal University, Beijing, China

    Guohui Wang, Yong Guan, Qianying Zhang, Xiaojuan Li & Yongdong Li

  2. School of Mathematical Science, Capital Normal University, Beijing, China

    Guohui Wang

  3. Beijing Key Laboratory of Light Industrial Robot and Safety Verification, College of Information Engineering, Capital Normal University, Beijing, China

    Yong Guan, Zhiping Shi & Xiaojuan Li

  4. Beijing Center for Mathematics and Information Interdisciplinary Sciences, Capital Normal University, Beijing, China

    Guohui Wang, Zhiping Shi & Qianying Zhang

  5. National International Science and Technology Cooperation Demonstration Base of Interdisciplinary of Electronic System Reliability and Mathematics, Capital Normal University, Beijing, China

    Yong Guan & Zhiping Shi

Authors
  1. Guohui Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yong Guan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Zhiping Shi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Qianying Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Xiaojuan Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Yongdong Li
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Guohui Wang or Zhiping Shi .

Editor information

Editors and Affiliations

  1. University of Auckland, Auckland, New Zealand

    Jing Sun

  2. Peking University, Beijing, China

    Meng Sun

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Wang, G., Guan, Y., Shi, Z., Zhang, Q., Li, X., Li, Y. (2018). Formalization of Symplectic Geometry in HOL-Light. In: Sun, J., Sun, M. (eds) Formal Methods and Software Engineering. ICFEM 2018. Lecture Notes in Computer Science(), vol 11232. Springer, Cham. https://doi.org/10.1007/978-3-030-02450-5_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02450-5_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-02449-9

  • Online ISBN: 978-3-030-02450-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation