Paper Info
Title
Formalization Of Euler-Lagrange Equation Set Based On Variational Calculus In Hol Light
Abstract
As the theoretical foundation of Lagrangian mechanics, Euler-Lagrange equation sets are widely applied in building mathematical models of physical systems, especially in solving dynamics problems. However, their preconditions are often not fully satisfied in practice. Therefore, it is necessary to verify their applications. The purpose of the present work is to conduct such verification by establishing a formal theorem library of Lagrangian mechanics in HOL Light. For this purpose, some basic concepts such as functional variation and the necessary conditions for functional extreme are formalized. Then, the fundamental lemma of variational calculus is formally verified and some new constuctors and destructors are proposed. Finally, the Euler-Lagrange equation set is formalized. To validate the formalization, the formalization results are applied to verify the least resistance problem of gas flow. The present work not only lays a necessary and solid foundation for application involving Lagrangian mechanics but also extends the HOL Light theorem library.
Year
DOI
Venue
2021
10.1007/s10817-020-09549-w
JOURNAL OF AUTOMATED REASONING
Keywords
DocType
Volume
Euler-Lagrange equation set, Functional variations, Dynamics analysis, Theorem proving
Journal
65
Issue
ISSN
Citations 
1
0168-7433
0
PageRank 
References 
Authors
0.34
0
6
Name
Order
Citations
PageRank
Yong Guan178782.67
Jingzhi Zhang2194.74
Guohui Wang303.04
Ximeng Li4105.27
Zhiping Shi516843.86
Li Y.611715.14