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

Formal Charges02:42

Formal Charges

32.9K
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.
32.9K
Constraints and Statical Determinacy01:26

Constraints and Statical Determinacy

667
In structural engineering, the equilibrium of a system is not only determined by its equations of equilibrium but also with the help of constraints. Constraints refer to restrictions on the motion of a system. The proper combinations of constraints can minimize the total number of constraints needed to maintain a system in mechanical equilibrium. When this happens, the system is said to be statically determinate. For such systems, the unknown reaction supports can be estimated using equilibrium...
667
Hückel's Rule Diagram of π MOs: Frost Circle01:08

Hückel's Rule Diagram of π MOs: Frost Circle

4.6K
The Frost circle or the inscribed polygon method is a graphical method for determining the relative energies of π molecular orbitals (MOs) for planar, fully conjugated, and monocyclic compounds. This method was first described by A. A. Frost and Boris Musulin in 1953.
A Frost circle is constructed by drawing a polygon whose number of edges is equal to the number of carbons of the given cyclic system, with one of the vertices pointing down. Then, a circle is drawn enclosing the polygon so...
4.6K
First-Order Circuits01:15

First-Order Circuits

1.6K
First-order electrical circuits, which comprise resistors and a single energy storage element - either a capacitor or an inductor, are fundamental to many electronic systems. These circuits are governed by a first-order differential equation that describes the relationship between input and output signals.
One common example of a first-order circuit is the RC (resistor-capacitor) circuit. These circuits are used in relaxation oscillators such as neon lamp oscillator circuits. When voltage is...
1.6K
First Order Systems01:21

First Order Systems

149
First-order systems, such as RC circuits, are foundational in understanding dynamic systems due to their straightforward input-output relationship. Analyzing their responses to different input functions under zero initial conditions reveals significant insights into system behavior.
When a first-order system is subjected to a unit-step input, its response is characterized by its transfer function. By applying the Laplace transform of the unit-step input to the transfer function, expanding the...
149
SFG Algebra01:16

SFG Algebra

160
In Signal Flow Graph (SFG) algebra, the value a node represents is determined by the sum of all signals entering that node. This summed value is then transmitted through every branch leaving the node, making the SFG a powerful tool for visualizing and analyzing control systems.
Each node in an SFG corresponds to a variable, and the interactions between nodes are represented by branches with associated gains. When multiple branches lead into a node, the value at that node is the sum of the...
160

You might also read

Related Articles

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

Sort by
Same author

Intelligent Sensor Software for Robust and Energy-Sustainable Decision-Making in Welding of Steel Reinforcement for Concrete.

Sensors (Basel, Switzerland)·2025
Same author

Analysis of Varroa Mite Colony Infestation Level Using New Open Software Based on Deep Learning Techniques.

Sensors (Basel, Switzerland)·2024
Same author

Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL.

Journal of automated reasoning·2020
Same author

A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm.

Journal of automated reasoning·2020
Same author

A Verified Implementation of Algebraic Numbers in Isabelle/HOL.

Journal of automated reasoning·2020

Related Experiment Video

Updated: Aug 22, 2025

Executing Complexity-Increasing Queries in Relational MySQL and NoSQL MongoDB and EXist Size-Growing ISO/EN 13606 Standardized EHR Databases
07:26

Executing Complexity-Increasing Queries in Relational MySQL and NoSQL MongoDB and EXist Size-Growing ISO/EN 13606 Standardized EHR Databases

Published on: March 19, 2018

9.4K

A Formalization of the Smith Normal Form in Higher-Order Logic.

Jose Divasón1, René Thiemann2

  • 1University of La Rioja, Logroño, Spain.

Journal of Automated Reasoning
|November 10, 2022
PubMed
Summary

This study provides formal correctness proofs for matrix Smith normal form algorithms using Isabelle/HOL. The proofs ensure algorithm soundness and cover the uniqueness of the Smith normal form in general settings.

Keywords:
Elementary divisor ringsIsabelle/HOLLocal type definitionsTheorem proving

More Related Videos

Using Eye Movements Recorded in the Visual World Paradigm to Explore the Online Processing of Spoken Language
09:27

Using Eye Movements Recorded in the Visual World Paradigm to Explore the Online Processing of Spoken Language

Published on: October 13, 2018

10.1K
One Dimensional Turing-Like Handshake Test for Motor Intelligence
14:05

One Dimensional Turing-Like Handshake Test for Motor Intelligence

Published on: December 15, 2010

27.4K

Related Experiment Videos

Last Updated: Aug 22, 2025

Executing Complexity-Increasing Queries in Relational MySQL and NoSQL MongoDB and EXist Size-Growing ISO/EN 13606 Standardized EHR Databases
07:26

Executing Complexity-Increasing Queries in Relational MySQL and NoSQL MongoDB and EXist Size-Growing ISO/EN 13606 Standardized EHR Databases

Published on: March 19, 2018

9.4K
Using Eye Movements Recorded in the Visual World Paradigm to Explore the Online Processing of Spoken Language
09:27

Using Eye Movements Recorded in the Visual World Paradigm to Explore the Online Processing of Spoken Language

Published on: October 13, 2018

10.1K
One Dimensional Turing-Like Handshake Test for Motor Intelligence
14:05

One Dimensional Turing-Like Handshake Test for Motor Intelligence

Published on: December 15, 2010

27.4K

Area of Science:

  • Computer Science
  • Formal Methods
  • Computational Algebra

Background:

  • Matrix computations are fundamental in various scientific and engineering fields.
  • Canonical forms like Smith normal form simplify matrix analysis and problem-solving.
  • Formal verification ensures the reliability of algorithms used in critical applications.

Purpose of the Study:

  • To formally prove the correctness of algorithms for transforming matrices into Smith normal form.
  • To establish the soundness of these algorithms under general conditions and specific mathematical structures.
  • To provide formal proofs for the generality and uniqueness of the Smith normal form.

Main Methods:

  • Utilizing the Isabelle/HOL theorem prover for formal verification.
  • Developing abstract algorithms parameterized by basic operations.
  • Employing the lifting and transfer package and local type definitions for HOL extension.

Main Results:

  • Formal correctness proofs for Smith normal form algorithms in Isabelle/HOL.
  • Demonstrated soundness of algorithms on Euclidean domains.
  • Formal proofs of algorithm generality and Smith normal form uniqueness.

Conclusions:

  • The formal proofs establish the reliability of the presented Smith normal form algorithms.
  • The abstract approach ensures applicability across various mathematical structures.
  • The use of Isabelle/HOL with specific techniques enables formal verification in the absence of dependent types.