Abstract
Fourier transform based techniques are widely used for solving differential equations and to perform the frequency response analysis of signals in many safety-critical systems. To perform the formal analysis of these systems, we present a formalization of Fourier transform using higher-order logic. In particular, we use the HOL-Light’s differential, integral, transcendental and topological theories of multivariable calculus to formally define Fourier transform and reason about the correctness of its classical properties, such as existence, linearity, frequency shifting, modulation, time reversal and differentiation in time-domain. In order to demonstrate the practical effectiveness of the proposed formalization, we use it to formally verify the frequency response of an automobile suspension system.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Beerends, R.J., Morsche, H.G., Van den Berg, J.C., Van de Vrie, E.M.: Fourier and Laplace Transforms. Cambridge University Press, Cambridge (2003)
Bracewell, R.N.: The Fourier Transform and its Applications. McGraw-Hill, New York (1978)
Du, K.L., Swamy, M.N.S.: Wireless Communication Systems: from RF Subsystems to 4G Enabling Technologies. Cambridge University Press, Cambridge (2010)
Khan-Afshar, S., Siddique, U., Mahmoud, M.Y., Aravantinos, V., Seddiki, O., Hasan, O., Tahar, S.: Formal analysis of optical systems. Math. Comput. Sci. 8(1), 39–70 (2014)
Oppenheim, A.V., Willsky, A.S., Hamid Nawab, S.: Signals and Systems. Prentice Hall Processing Series, 2nd edn. Prentice Hall, Inc., Englewood Cliffs (1996)
Rashid, A.: On the Formalization of Fourier Transform in Higher-order Logic (2016). http://save.seecs.nust.edu.pk/projects/fourier/
Siddique, U., Mahmoud, M.Y., Tahar, S.: On the formalization of Z-transform in HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 483–498. Springer, Heidelberg (2014)
Taqdees, S.H., Hasan, O.: Formalization of laplace transform using the multivariable calculus theory of HOL-light. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 744–758. Springer, Heidelberg (2013)
Yang, X.S.: Mathematical Modeling with Multidisciplinary Applications. Wiley, Hoboken (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Rashid, A., Hasan, O. (2016). On the Formalization of Fourier Transform in Higher-order Logic. In: Blanchette, J., Merz, S. (eds) Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer Science(), vol 9807. Springer, Cham. https://doi.org/10.1007/978-3-319-43144-4_31
Download citation
DOI: https://doi.org/10.1007/978-3-319-43144-4_31
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-43143-7
Online ISBN: 978-3-319-43144-4
eBook Packages: Computer ScienceComputer Science (R0)