文章基本信息

标题：Formalization of Matrix Theory in HOL4:
本地全文：下载
作者：Zhiping Shi ; Yan Zhang ; Zhenke Liu 等
期刊名称：Advances in Mechanical Engineering
印刷版ISSN：1687-8140
电子版ISSN：1687-8140
出版年度：2014
卷号：6
页码：1-16
DOI：10.1155/2014/195276
语种：English
出版社：Sage Publications Ltd.
摘要：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.