Enabling Symbolic and Numerical Computations in HOL Light

摘要

Verifying mathematical statements by interactive theorem provers often requires algebraic computation. Since many Mechanized Mathematical Systems (MMS) support the OpenMath standard, we propose to link the HOL Light theorem prover to other MMSs via Open-Math. In particular, we present an interface between HOL Light and Mathematica enabling HOL Light users to evaluate arithmetic, transcendental and linear algebraic expressions, using Mathematica.