Formalization of Matrix Theory in HOL4 | Zendy

Shi Zhiping | Zendy; Zhang Yan | Zendy; Liu Zhenke | Zendy; Kang Xinan | Zendy; Guan Yong | Zendy; Zhang Jie | Zendy; Song Xiaoyu | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Formalization of Matrix Theory in HOL4

Author(s) -

Shi Zhiping,

Zhang Yan,

Liu Zhenke,

Kang Xinan,

Guan Yong,

Zhang Jie,

Song Xiaoyu

Publication year - 2014

Publication title -

advances in mechanical engineering

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.318

H-Index - 40

ISSN - 1687-8132

DOI - 10.1155/2014/195276

Subject(s) - hol , computer science , matrix (chemical analysis) , algebra over a field , theoretical computer science , state transition matrix , mathematics , symmetric matrix , pure mathematics , materials science , composite material , programming language , eigenvalues and eigenvectors , physics , quantum mechanics

Matrix theory plays an important role in modeling linear systems in engineering and science. To model and analyze the intricate behavior of complex systems, it is imperative to formalize matrix theory in a metalogic setting. This paper presents the higher-order logic (HOL) formalization of the vector space and matrix theory in the HOL4 theorem proving system. Formalized theories include formal definitions of real vectors and matrices, algebraic properties, and determinants, which are verified in HOL4. Two case studies, modeling and verifying composite two-port networks and state transfer equations, are presented to demonstrate the applicability and effectiveness of our work.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research