Formalization of Matrix Theory in HOL4
Formalization of Matrix Theory in HOL4
复制标题
HOL4 中矩阵理论的形式化
DOI：
10.1155/2014/195276
复制
发表时间：
2014-01-01
影响因子：
2.1
通讯作者：
Song, Xiaoyu
中科院分区：
文献类型：
--
作者：
Shi, Zhiping;Zhang, Yan;Song, Xiaoyu
矩阵理论在建模工程和科学中的线性系统中起着重要作用。为了对复杂系统的复杂行为进行建模和分析，必须在金属含量环境中形式化基质理论。本文介绍了HOL4定理证明系统中向量空间和矩阵理论的高阶逻辑（HOL）形式化。形式化的理论包括对实际媒介和矩阵的形式定义，代数性质和决定因素，这些定义已在HOL4中进行了验证。提出了两项案例研究，即建模和验证复合材料两端口网络和状态转移方程，以证明我们工作的适用性和有效性。
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.