Affiliations: [a] School of Information Science and Engineering, Yunnan University, Kunming, Yunnan 650091, China | [b] College of Information Science and Engineering, Northeastern University, Shenyang, Liaoning 110819, China
Correspondence:
[*]
Corresponding author: Chunna Zhao, School of Information Science and Engineering, Yunnan University, Kunming, Yunnan 650091, China. E-mail: [email protected].
Abstract: There are three kinds of commonly used fractional calculus definitions. And they are Grünwald-Letnikov (GL) calculus, Riemann-Liouville (RL) calculus, and Caputo calculus. Relationship among GL, RL and Caputo calculus is the basis for formalization of fractional order control systems. Higher order logic theorem proving method is applied to construe the relationship in this paper. The essential differences among these three definitions are introduced firstly. Relationship between GL calculus and Caputo calculus is verified by a higher order logic theorem prover. And then the relationship between RL definition and Caputo calculus is also formalized in this paper. The study provides a good research foundation for formal verification of fractional order PI controller. The fractional order PI controller in a humanoid robot system has been verified based on the formalization of fractional calculus. Results show that fractional order PI controller is very effective and reliable. And it also shows that the formalization of fractional calculus definitions is correct. It provides the research method for formalization of fractional order control systems.
Keywords: Fractional calculus, theorem proving, higher order logic, formalization
