Skip to main content
main-content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

06.03.2020

Formalization of Euler–Lagrange Equation Set Based on Variational Calculus in HOL Light

Zeitschrift:
Journal of Automated Reasoning
Autoren:
Yong Guan, Jingzhi Zhang, Guohui Wang, Ximeng Li, Zhiping Shi, Yongdong Li
Wichtige Hinweise

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

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.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

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




Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

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




Testen Sie jetzt 30 Tage kostenlos.

Literatur
Über diesen Artikel

Premium Partner

    Bildnachweise