Abstract
Complex vector analysis is widely used to analyze continuous systems in many disciplines, including physics and engineering. In this paper, we present a higher-order-logic formalization of the complex vector space to facilitate conducting this analysis within the sound core of a theorem prover: HOL Light. Our definition of complex vector builds upon the definitions of complex numbers and real vectors. This extension allows us to extensively benefit from the already verified theorems based on complex analysis and real vector analysis. To show the practical usefulness of our library we adopt it to formalize electromagnetic fields and to prove the law of reflection for the planar waves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Afshar, S.K., Aravantinos, V., Hasan, O., Tahar, S.: A toolbox for complex linear algebra in HOL Light. Technical Report, Concordia University, Montreal, Canada (2014)
Afshar, S.K., Siddique, U., Mahmoud, M.Y., Aravantinos, V., Seddiki, O., Hasan, O., Tahar, S.: Formal analysis of optical systems. Mathematics in Computer Science 8(1) (2014)
Chaieb, A.: Multivariate Analysis (2014), http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Multivariate_Analysis
Gibbs, J.W.: Elements of Vectors Analysis. Tuttle, Morehouse & Taylor (1884)
Harrison, J.: Formalizing basic complex analysis. In: From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric, pp. 151–165. University of Białystok (2007)
Harrison, J.: HOL Light: An Overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009)
Harrison, J.: The HOL Light theory of Euclidean space. Journal of Automated Reasoning 50(2), 173–190 (2013)
Herencia-Zapana, H., Jobredeaux, R., Owre, S., Garoche, P.-L., Feron, E., Perez, G., Ascariz, P.: PVS linear algebra libraries for verification of control software algorithms in C/ACSL. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 147–161. Springer, Heidelberg (2012)
LePage, W.R.: Complex variables and the Laplace transform for engineers. Dover Publications (1980)
Mahmoud, M.Y., Aravantinos, V., Tahar, S.: Formalization of infinite dimension linear spaces with application to quantum theory. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 413–427. Springer, Heidelberg (2013)
Scharnhorst, K.: Angles in complex vector spaces. Acta Applicandae Mathematica 69(1), 95–103 (2001)
Stein, J.: Linear Algebra (2014), http://coq.inria.fr/pylons/contribs/view/LinAlg/trunk
Tallack, J.C.: Introduction to Vector Analysis. Cambridge University Press (1970)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Afshar, S.K., Aravantinos, V., Hasan, O., Tahar, S. (2014). Formalization of Complex Vectors in Higher-Order Logic. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds) Intelligent Computer Mathematics. CICM 2014. Lecture Notes in Computer Science(), vol 8543. Springer, Cham. https://doi.org/10.1007/978-3-319-08434-3_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-08434-3_10
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08433-6
Online ISBN: 978-3-319-08434-3
eBook Packages: Computer ScienceComputer Science (R0)