Formal Analysis of Electromagnetic Optics Models in HOL
Light, as an electromagnetic wave phenomenon, is described by the
same theoretical principles that govern all forms of electromagnetic
radiation.
We employ theorem proving as a complement to computational
and numerical approaches to improve optical model analysis
in a formal analysis framework. We provide the formalization of fundamental
physical theories and laws to reason about the behaviour of light
as electromagnetic waves in higher-order logic to verify its key properties
using the HOL Light theorem prover.
We also plan to formalize necessary mathematical background to model an optical device based on electromagnetic theory.
We have formalized some fundamentals of Electromagnetic optics.
[1] O. Hasan, S.K. Afshar, and S. Tahar: Formal Analysis of Optical Waveguides in HOL S. Berghofer et al. (Eds.), Theorem Proving in Higher-Order Logics, Lecture Notes in Computer Science 5674, Springer Verlag, 2009, pp. 228-243. [Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'09), Munich, Germany, August 2009.]
HOL Code Scripts
References
[1] O. Hasan, S.K. Afshar, and S. Tahar: Formal Analysis of Optical Waveguides in HOL S. Berghofer et al. (Eds.), Theorem Proving in Higher-Order Logics, Lecture Notes in Computer Science 5674, Springer Verlag, 2009, pp. 228-243. [Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'09), Munich, Germany, August 2009.]
