Formalization of Matrix Theory in HOL4

Authors

Zhiping Shi, Chinese Academy of SciencesFollow
Yan Zhang, Capital Normal University
Zhenke Liu, Capital Normal University
Xinan Kang, Capital Normal University
Yong Guan, Capital Normal UniversityFollow
Jie Zhang, Beijing University of Chemical TechnologyFollow
Xiaoyu Song, Portland State UniversityFollow

Published In

Advances in Mechanical Engineering

Document Type

Article

Publication Date

8-28-2014

Subjects

Matrices, Number theory, Dynamical systems, Vector fields

Abstract

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 higherorder 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.

Description

Copyright © 2014 Zhiping Shi et al. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

DOI

10.1155/2014/195276

Persistent Identifier

http://archives.pdx.edu/ds/psu/15670

Citation Details

Shi, Z., Zhang, Y., Liu, Z., Kang, X., Guan, Y., Zhang, J., & Song, X. (2014). Formalization of matrix theory in HOL4. Advances in Mechanical Engineering, 6, 195276.