Affiliation of Author(s):计算机科学与技术学院/人工智能学院/软件学院
Journal:Proc. IEEE Int. Conf. Saf. Prod. Informatiz., IICSPI
Abstract:In our previous work, we have introduced a formal definition of Laplace transform in Coq, and proved a group of basic properties of Laplace transform, including linear property, frequency shifting and first order differentiation. However, in many control systems, Laplace transforms are often applied on functions containing second-order derivatives and integrals with variable upper bound. This paper extends our previous results by adding formal Coq proofs on properties of these two kinds of Laplace transforms. Finally, as an application of these formal properties, we presents a formal derivation of the transfer function of a DC motor control system for robots. © 2018 IEEE.
Translation or Not:no
Date of Publication:2019-04-12
Co-author:Gang Chen
Correspondence Author:wangyifei
Date of Publication:2019-04-12