Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
type: Item
instance of: scholarly article
title: Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
author: Yong Guan
author: Jingzhi Zhang
author: Guohui Wang
author: Ximeng Li
author: Zhiping Shi
author: Yong-Dong Li
published in: Journal of Automated Reasoning
publication date: 2021-06-09T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7356966
zbMATH Keywords: Euler-Lagrange equation set
zbMATH Keywords: functional variations
zbMATH Keywords: dynamics analysis
zbMATH Keywords: theorem proving
describes a project that uses: HOL Light
describes a project that uses: Sledgehammer
describes a project that uses: ACL2
describes a project that uses: HOL
describes a project that uses: GitHub
MaRDI profile type: Publication
full work available at URL: s10817-020-09549-w
OpenAlex ID: W3010056057
cites work: Formulation of Euler-Lagrange equations for fractional variational problems
cites work: Automatic Proof and Disproof in Isabelle/HOL
cites work: Q5842044
cites work: Formalization of real analysis: a survey of proof assistants and libraries
cites work: A problem on brachistochrone as invariant variational problem
cites work: Q4528914
cites work: Applications of real number theorem proving in PVS
cites work: Global and local variational derivatives and integral representations of Gateaux differentials
cites work: HOL Light: An Overview
cites work: The HOL Light theory of Euclidean space
cites work: Variational principles for some nonlinear partial differential equations with variable coefficients
cites work: Q4230801
cites work: Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm
cites work: On a fundamental theorem of the calculus of variations
cites work: Formal analysis of the kinematic Jacobian in screw theory
cites work: A Brief Overview of HOL4
cites work: ATP and presentation service for Mizar formalizations
cites work: Formalization of functional variation in HOL Light
cites work: Formalization of fractional order PD control systems in HOL4
DOI: 10.1007/S10817-020-09549-W
description: scientific article; zbMATH DE number 7356966