On the Formal Analysis of Geometrical Optics in HOL

DOI10.1007/978-3-642-40672-0_11zbMath1396.68114OpenAlexW1417172323MaRDI QIDQ2849513

Vincent Aravantinos, Umair Siddique, Sofiène Tahar

Publication date: 20 September 2013

Published in: Automated Deduction in Geometry (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-40672-0_11

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Geometric optics (78A05)

Related Items (5)

Formal verification of stability and chaos in periodic optical systems ⋮ On the formal analysis of Gaussian optical systems in HOL ⋮ On the Formalization of Cardinal Points of Optical Systems ⋮ Formal analysis of optical systems ⋮ A Framework for Formal Reasoning about Geometrical Optics

Uses Software

• Isabelle/HOL
• HOL
• HOL Light
• LASCAD

This page was built for publication: On the Formal Analysis of Geometrical Optics in HOL