Jove
Visualize
Contact Us
JoVE
x logofacebook logolinkedin logoyoutube logo
ABOUT JoVE
OverviewLeadershipBlogJoVE Help Center
AUTHORS
Publishing ProcessEditorial BoardScope & PoliciesPeer ReviewFAQSubmit
LIBRARIANS
TestimonialsSubscriptionsAccessResourcesLibrary Advisory BoardFAQ
RESEARCH
JoVE JournalMethods CollectionsJoVE Encyclopedia of ExperimentsArchive
EDUCATION
JoVE CoreJoVE BusinessJoVE Science EducationJoVE Lab ManualFaculty Resource CenterFaculty Site
Terms & Conditions of Use
Privacy Policy
Policies

Related Concept Videos

MO Theory and Covalent Bonding02:40

MO Theory and Covalent Bonding

12.1K
The molecular orbital theory describes the distribution of electrons in molecules in a manner similar to the distribution of electrons in atomic orbitals. The region of space in which a valence electron in a molecule is likely to be found is called a molecular orbital. Mathematically, the linear combination of atomic orbitals (LCAO) generates molecular orbitals. Combinations of in-phase atomic orbital wave functions result in regions with a high probability of electron density, while...
12.1K
Molecular Orbital Theory II03:51

Molecular Orbital Theory II

20.3K
Molecular Orbital Energy Diagrams
20.3K
Relation between Mathematical Equations and Block Diagrams01:20

Relation between Mathematical Equations and Block Diagrams

2.2K
In a spring-mass-damper system, the second-order differential equation describes the dynamic behavior of the system. When transformed into the Laplace domain under zero initial conditions, this equation can be effectively analyzed and manipulated. The transformation into the Laplace domain converts differential equations into algebraic equations, simplifying the process of isolating the output.
2.2K
Formal Charges02:42

Formal Charges

35.1K
In some cases, there are seemingly more than one valid Lewis structures for molecules and polyatomic ions. The concept of formal charges can be used to help predict the most appropriate Lewis structure when more than one reasonable structure exists.
35.1K
Valence Bond Theory02:45

Valence Bond Theory

35.5K
Overview of Valence Bond Theory
35.5K
Valence Bond Theory and Hybridized Orbitals02:38

Valence Bond Theory and Hybridized Orbitals

23.9K
According to valence bond theory, a covalent bond results when: (1) an orbital on one atom overlaps an orbital on a second atom, and (2) the single electrons in each orbital combine to form an electron pair. The strength of a covalent bond depends on the extent of overlap of the orbitals involved. Maximum overlap is possible when the orbitals overlap on a direct line between the two nuclei.
A σ bond (single bond in a Lewis structure) is a covalent bond in which the electron density is...
23.9K

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by
Same author

Formal Verification of Deep Brain Stimulation Controllers for Parkinson's Disease Treatment.

Neural computation·2023
Same author

Effects of social and emotional context on neural activation and synchrony during movie viewing.

Human brain mapping·2021
Same author

Chronic kidney disease diagnosis using decision tree algorithms.

BMC nephrology·2021
Same author

Formal verification of Matrix based MATLAB models using interactive theorem proving.

PeerJ. Computer science·2021
Same author

How childhood diseases awareness contributes to minimize the risk of disease severity in children under five age: An evolutionary study.

JPMA. The Journal of the Pakistan Medical Association·2021
Same author

Formal reasoning about synthetic biology using higher-order-logic theorem proving.

IET systems biology·2020
Same journal

Enhancing interpretable soft sensing with embedded hybrid modeling: the GraphTrans approach for industrial processes.

ISA transactions·2026
Same journal

Exploiting underutilized heterogeneous data: A multi-source domain adaptive siamese network for few-shot bearing fault diagnosis.

ISA transactions·2026
Same journal

Prescribed performance synchronization control of dual-PMSM motion system via novel sliding mode control and adaptive extended state observer.

ISA transactions·2026
Same journal

A Teager energy operator-informed shrinkage residual network for end-to-end noise-robust fault diagnosis of rotating machinery.

ISA transactions·2026
Same journal

Finite-time swing attenuation for differentially flat quadrotor slung-load systems via robust AFITSM-OSMC partitioned control.

ISA transactions·2026
Same journal

Energy-efficient exact-time chattering-free recursive sliding mode control of UUVs based on disturbance observer.

ISA transactions·2026
See all related articles

Related Experiment Video

Updated: Oct 8, 2025

Author Spotlight: Functionalizing Metal-Organic Frameworks: Advancements, Challenges, and the Power of Post-Synthetic Ligand Exchange
04:51

Author Spotlight: Functionalizing Metal-Organic Frameworks: Advancements, Challenges, and the Power of Post-Synthetic Ligand Exchange

Published on: June 23, 2023

3.5K

Formalization of bond graph using higher-order-logic theorem proving.

Ujala Qasim1, Adnan Rashid2, Osman Hasan2

  • 1Research Center for Modeling and Simulations (RCMS), National University of Sciences and Technology (NUST), Islamabad, Pakistan.

ISA Transactions
|January 1, 2022
PubMed
Summary
This summary is machine-generated.

Higher-order-logic theorem proving offers accurate dynamical analysis for complex systems. This study formalizes bond graphs and verifies stability properties, demonstrated on a prosthetic hand.

Keywords:
Bond graphsHOL LightHigher-order logicState–space modelsTheorem proving

More Related Videos

Synthesis of a Thiol Building Block for the Crystallization of a Semiconducting Gyroidal Metal-sulfur Framework
12:30

Synthesis of a Thiol Building Block for the Crystallization of a Semiconducting Gyroidal Metal-sulfur Framework

Published on: April 9, 2018

9.2K
Author Spotlight: Experimental Approaches for the Synthesis of Low-Valent Metal-Organic Frameworks from Multitopic Phosphine Linkers
07:14

Author Spotlight: Experimental Approaches for the Synthesis of Low-Valent Metal-Organic Frameworks from Multitopic Phosphine Linkers

Published on: May 12, 2023

3.2K

Related Experiment Videos

Last Updated: Oct 8, 2025

Author Spotlight: Functionalizing Metal-Organic Frameworks: Advancements, Challenges, and the Power of Post-Synthetic Ligand Exchange
04:51

Author Spotlight: Functionalizing Metal-Organic Frameworks: Advancements, Challenges, and the Power of Post-Synthetic Ligand Exchange

Published on: June 23, 2023

3.5K
Synthesis of a Thiol Building Block for the Crystallization of a Semiconducting Gyroidal Metal-sulfur Framework
12:30

Synthesis of a Thiol Building Block for the Crystallization of a Semiconducting Gyroidal Metal-sulfur Framework

Published on: April 9, 2018

9.2K
Author Spotlight: Experimental Approaches for the Synthesis of Low-Valent Metal-Organic Frameworks from Multitopic Phosphine Linkers
07:14

Author Spotlight: Experimental Approaches for the Synthesis of Low-Valent Metal-Organic Frameworks from Multitopic Phosphine Linkers

Published on: May 12, 2023

3.2K

Area of Science:

  • Engineering
  • Computer Science
  • Formal Methods

Background:

  • Bond graphs are a graphical method for analyzing complex system dynamics across various fields.
  • Traditional analysis methods (paper-and-pencil, computational) have limitations including errors, approximations, and high computational costs.
  • These limitations make traditional methods unsuitable for safety-critical systems in robotics and medicine.

Purpose of the Study:

  • To propose and formalize the use of higher-order-logic theorem proving for bond graph-based dynamical analysis.
  • To develop functions for converting bond graphs to state-space models and verifying system properties like stability.
  • To demonstrate the practical application and effectiveness of this formal approach.

Main Methods:

  • Formalization of bond graphs using higher-order-logic theorem proving.
  • Development of functions for automated conversion to state-space models.
  • Implementation of stability verification for physical systems.
  • Application of HOL Light theorem prover for formal stability analysis of a prosthetic mechatronic hand.
  • Encoding verified theorems in MATLAB for accessibility to non-experts.

Main Results:

  • Successful formalization of bond graphs and their conversion to state-space models.
  • Demonstrated formal verification of system properties, specifically stability.
  • Practical application showcased through the stability analysis of a prosthetic mechatronic hand.
  • MATLAB encoding of verified theorems to facilitate broader use.

Conclusions:

  • Higher-order-logic theorem proving provides a robust and accurate alternative to traditional methods for bond graph analysis.
  • The proposed formalization and verification approach enhances the reliability of dynamical analysis, especially for safety-critical systems.
  • The integration with MATLAB makes advanced formal methods more accessible for analyzing complex systems like prosthetic devices.