nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Formalization of Symplectic Geometry in HOL-Light

verfasst von : Guohui Wang, Yong Guan, Zhiping Shi, Qianying Zhang, Xiaojuan Li, Yongdong Li

Erschienen in: Formal Methods and Software Engineering

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel A Framework for Interactive Verification of Architectural Design Patterns in Isabelle/HOL

Nächstes Kapitel Using Theorem Provers to Increase the Precision of Dependence Analysis for Information Flow Control

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-9265MathSciNetCrossRefMATH

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

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_2CrossRef

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

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

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

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)CrossRef

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_4CrossRef

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

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)

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)MathSciNetCrossRef

12.

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

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)MathSciNetCrossRef

14.

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

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)

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_6CrossRef

17.

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

18.

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

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)CrossRef

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)CrossRef

21.

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

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)

Titel: Formalization of Symplectic Geometry in HOL-Light
verfasst von: Guohui Wang
Yong Guan
Zhiping Shi
Qianying Zhang
Xiaojuan Li
Yongdong Li
Verlag: Springer International Publishing
Buch: Formal Methods and Software Engineering
Print ISBN: 978-3-030-02449-9

Electronic ISBN: 978-3-030-02450-5

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-030-02450-5_16

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"