Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
From MaRDI portal
Publication:2031406
DOI10.1007/s10817-020-09549-wOpenAlexW3010056057MaRDI QIDQ2031406
Ximeng Li, Yong-Dong Li, Jingzhi Zhang, Zhiping Shi, Yong Guan, Guo-hui Wang
Publication date: 9 June 2021
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-020-09549-w
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Applications of real number theorem proving in PVS
- A problem on brachistochrone as invariant variational problem
- On a fundamental theorem of the calculus of variations
- Global and local variational derivatives and integral representations of Gateaux differentials
- Variational principles for some nonlinear partial differential equations with variable coefficients
- Formal analysis of the kinematic Jacobian in screw theory
- Formalization of fractional order PD control systems in HOL4
- Formulation of Euler-Lagrange equations for fractional variational problems
- The HOL Light theory of Euclidean space
- ATP and presentation service for Mizar formalizations
- Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm
- Formalization of functional variation in HOL Light
- Formalization of real analysis: a survey of proof assistants and libraries
- Automatic Proof and Disproof in Isabelle/HOL
- HOL Light: An Overview
- A Brief Overview of HOL4
This page was built for publication: Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
