Formalization of Function Matrix Theory in HOL4
Xiaojuan Li · Journal of Chinese Computer Systems · 2013
Theorem proving is one of the most important methods of formal verification,it model the system for logic formula,reasoning and complete verification relying on theorem prover.The more the theorem prover contains theorem library,the stronger its reasoning ability.Function matrices are widely used in the control theory to describe state space.Formalizing the function matrix theory is significant for the formal analysis of control systems.Based on the higher order logical theorem prover Higher-Order Logic 4,this paper formalizes the function vector and function matrix theory,including data types,operations and their properties.The paper also presents the formal definition of the function matrix derivative,proves the commonly used theorems of the function matrix(or function vector) differential on quantity variables and presents the formal proof of quadratic function derivative.The formalization is implemented as a library in the Higher-Order Logic 4 system.