Hardware Verification Group Home > Research > Frameworks > Optics >
Bridge between Computer Algebra and Theorem Prover
The use of Theorem Proving Systems (TPSs) over conventional methods in analysing complex optical systems is advantageous due to the inherent soundness and completeness. However, some sophisticated mathematical theories need other Mechanized Mathematical Systems (MMSs) to be solved. This issue is due to the fact that we cannot find symbolic (or closed-form) solutions to be able to formalize it in TPSs. Hence, we need to call Computer Algebra Systems (CASs) or numerical approaches to overcome this problem. We present a general architecture to combine multiple mechanized systems. Our method is based on the use of the OpenMath standard. We describe our approach by establishing a link between HOL Light as a theorem prover and Mathematica as a Computer Algebra System (see the figure below). Finally, we illustrate our work by evaluating eigenvalues of a real matrix.
Source Code
