Members

• Ons Seddiki
• Sanaz Khan Afshar
• Cvetan Dunchev
• Sofiène Tahar

Description

This project proposes a general architecture to connect HOL Light, a higher-order logic theorem prover, to mechanized mathematical systems, based on the use of the mathematical standard OpenMath. In particular, we implemented a prototype tool linking HOL Light to Mathematica as a Computer Algebra System through OpenMath. We developed a HOL Light translator which converts HOL Light statements into OpenMath objects and vice-versa. We also use a Phrasebook to connect OpenMath to Mathematica as illustrated in the figure below. Our prototype tool (HolMatica) is available for download at the web link provided below. It has been applied on several running examples such as evaluating eigenvalues of a real matrix.

Source Code

• Installation Guide
  
• HOL_Light_Mathematica.zip (This file contains all the source code of the application)
• Running_examples.txt (This file contains some examples)
• Demo (Demonstration of our tool on a running example)

Publications

1. S. K. Afshar, U. Siddique, M.Y. Mahmoud, V. Aravantinos, O. Seddiki, O. Hasan and S. Tahar: Formal Analysis of Optical Systems; Mathematics in Computer Science, Vol. 8, No. 1, Springer, May 2014, pp. 39-70.
2. O. Seddiki, C. Dunchev, S. Khan-Afshar and S. Tahar: Enabling Symbolic and Numerical Computations in HOL Light; In: M. Kerber, J. Carette, C. Kaliszyk, F. Rabe and V. Sorge (Eds.), Intelligent Computer Mathematics, Lecture Notes in Computer Science Volume 9150, pp 353-358 [Proc. Conference of Intelligent Computer Mathematics (CICM'2015), Washington, DC, July, 2015]