Formalization of Function Matrix Theory in HOL

Zhiping Shi, Zhenke Liu, Yong Guan, Shiwei Ye, Jie Zhang and Hongxing Wei

Journal of Applied Mathematics, 2014, vol. 2014, issue 1

Abstract: 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.

Date: 2014
References: Add references at CitEc
Citations:

Downloads: (external link)
https://doi.org/10.1155/2014/201214

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:wly:jnljam:v:2014:y:2014:i:1:n:201214

Access Statistics for this article

More articles in Journal of Applied Mathematics from John Wiley & Sons
Bibliographic data for series maintained by Wiley Content Delivery ().