Formalization of Function Matrix Theory in HOL
Joint Authors
Wei, Hongxing
Liu, Zhenke
Ye, Shiwei
Zhang, Jie
Guan, Yong
Shi, Zhiping
Source
Journal of Applied Mathematics
Issue
Vol. 2014, Issue 2014 (31 Dec. 2014), pp.1-10, 10 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2014-07-24
Country of Publication
Egypt
No. of Pages
10
Main Subjects
Abstract EN
Function matrices, in which elements are functions rather than numbers, are widely used in model analysis of dynamic systems such as control systems and robotics.
In safety-critical applications, the dynamic systems are required to be analyzed formally and accurately to ensure their correctness and safeness.
Higher-order logic (HOL) theorem proving is a promise technique to match the requirement.
This paper proposes a higher-order logic formalization of the function vector and the function matrix theories using the HOL theorem prover, including data types, operations, and their properties, and further presents formalization of the differential and integral of function vectors and function matrices.
The formalization is implemented as a library in the HOL system.
A case study, a formal analysis of differential of quadratic functions, is presented to show the usefulness of the proposed formalization.
American Psychological Association (APA)
Shi, Zhiping& Liu, Zhenke& Guan, Yong& Ye, Shiwei& Zhang, Jie& Wei, Hongxing. 2014. Formalization of Function Matrix Theory in HOL. Journal of Applied Mathematics،Vol. 2014, no. 2014, pp.1-10.
https://search.emarefa.net/detail/BIM-453960
Modern Language Association (MLA)
Shi, Zhiping…[et al.]. Formalization of Function Matrix Theory in HOL. Journal of Applied Mathematics No. 2014 (2014), pp.1-10.
https://search.emarefa.net/detail/BIM-453960
American Medical Association (AMA)
Shi, Zhiping& Liu, Zhenke& Guan, Yong& Ye, Shiwei& Zhang, Jie& Wei, Hongxing. Formalization of Function Matrix Theory in HOL. Journal of Applied Mathematics. 2014. Vol. 2014, no. 2014, pp.1-10.
https://search.emarefa.net/detail/BIM-453960
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-453960