INTRODUCTION TO HOL4 THEOREM PROVER

The HOL4 interactive theorem prover is a proof assistant based on Higher-Order Logic. It is an ML language based programming environment in which mathematical functions and predicates can be defined and theorems can be proven. The core of the HOL4 theorem prover is composed of a small set of axioms and inference rules, making proofs in HOL4 sound and trustable. The HOL4 prover includes several theories (libraries) that cover most subjects of classical mathematics. The tool also provides a set of built-in decision procedures that can help automatically prove many simple theorems of arithmetic and Boolean algebra. In this paper we provide an introduction to the HOL theorem prover and show how this tool can be used in the formal analysis of advanced mathematics problems.