Open AccessFormalization of Function Matrix Theory in HOL
Author(s) -
Zhiping Shi,
Zhenke Liu,
Yong Guan,
Shiwei Ye,
Jie Zhang,
Hongxing Wei
Publication year - 2014
Publication title -
journal of applied mathematics
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.307
H-Index - 43
eISSN - 1687-0042
pISSN - 1110-757X
DOI - 10.1155/2014/201214
Subject(s) - hol , correctness , automated theorem proving , function (biology) , computer science , higher order logic , matrix (chemical analysis) , differential (mechanical device) , mathematics , algorithm , algebra over a field , theoretical computer science , programming language , pure mathematics , description logic , materials science , evolutionary biology , engineering , composite material , biology , aerospace engineering
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
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom