Formalization of fractional order PD control systems in HOL4

Higher-order logic theorem proving method is applied to analyze fractional order PD control systems in this paper. Theorem proving is based on rigorous logic and correct mathematics theory. Firstly, existent conditions and formal model of fractional calculus Caputo definition is established in higher order logic theorem prover. Then some properties are verified, including homogeneity, linearity property, fractional differential of constant and relationship between integer order differential and fractional differential. And formalization of Laplace transform based on fractional calculus Caputo definition is given and we apply it to illustrate advantages of fractional calculus Caputo definition. Initial values based on fractional calculus Caputo definition have exact physical meanings. And then formal modeling of fractional order PD controller is verified based on the above properties. We also verify the stability and other properties of fractional order PD controller by theorem proving method. Lastly, steady-state error is analyzed based on formalization of fractional calculus Caputo definition. It shows that fractional order PD controller can achieve a better control performance than integer order PD controller.