Name
Abstract | ||
|---|---|---|
Functional variation is an important fundamental mathematical theory widely used in engineering analysis, especially in dynamics based design. However, its formalization still remains unexplored and this makes the verification of dynamic properties of engineering structures quite cumbersome. The present paper aims at initiating the formalization of this theory. For this purpose, the function-space theory is first formalized and then it is formally proved that this continuous function space is a Banach space. Then, linear functionals based on this function space are formalized. Further, the functional variation in the Fréchet derivative form and its main properties are formalized. Then the necessary condition of functional extrema is formally verified. Lastly, we formally verify the continuous functional and mean value theorem of functional variation for demonstrating the application of the formalized functional variation. The present formalization work can serve as a foundation for the formal verification of dynamic behavior of mechanical systems. |
Year | DOI | Venue |
|---|---|---|
2019 | 10.1016/j.jlamp.2019.04.004 | Journal of Logical and Algebraic Methods in Programming |
Keywords | Field | DocType |
Functional variation,Fréchet derivative,Continuous function space,Theorem proving,HOL Light | HOL,Continuous function,Function space,Mathematical theory,Fréchet derivative,Banach space,Maxima and minima,Theoretical computer science,Mathematics,Formal verification | Journal |
Volume | Issue | ISSN |
106 | 1 | 2352-2208 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jingzhi Zhang | 1 | 19 | 4.74 |
| Guohui Wang | 2 | 0 | 3.04 |
| Zhiping Shi | 3 | 168 | 43.86 |
| Yong Guan | 4 | 787 | 82.67 |
| Yongdong Li | 5 | 0 | 0.34 |