Formalization of complex vectors in higher-order logic

DOI10.1007/978-3-319-08434-3_10MaRDI QIDQ5495918zbMATH OpenOpenAlexFDO

Authors Sanaz Khan-Afshar, Vincent Aravantinos, Osman Hasan, Sofiène Tahar

Publication date 7 August 2014

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1405.4034

Mathematics Subject Classification ID

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.

Recommendations

• Formalization of function matrix theory in HOL
• Formalization of linear space theory in the higher-order logic proving system
• On the formalization of Fourier transform in higher-order logic
• Formal Analysis of Optical Waveguides in HOL
• Formalization of complex analysis and matrix theory

Cites work

• Angles in complex vector spaces
• Formal analysis of optical systems
• Formalization of complex vectors in higher-order logic
• HOL Light: An Overview
• scientific article; zbMATH DE number 3732643 (Why is no real title available?)
• The HOL Light theory of Euclidean space

Cited in

(4)

• Formalization of function matrix theory in HOL
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
• Formalization of complex analysis and matrix theory
• Formalization of complex vectors in higher-order logic

Describes a project that uses

Uses Software

• HOL Light
• Isabelle

This page was built for publication: Formalization of complex vectors in higher-order logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5495918)