INTRODUCTION TO HOL4 THEOREM PROVER


Aksoy K., Tahar S., ZEREN Y.

SIGMA JOURNAL OF ENGINEERING AND NATURAL SCIENCES-SIGMA MUHENDISLIK VE FEN BILIMLERI DERGISI, vol.10, no.2, pp.237-243, 2019 (ESCI) identifier

  • Publication Type: Article / Article
  • Volume: 10 Issue: 2
  • Publication Date: 2019
  • Journal Name: SIGMA JOURNAL OF ENGINEERING AND NATURAL SCIENCES-SIGMA MUHENDISLIK VE FEN BILIMLERI DERGISI
  • Journal Indexes: Emerging Sources Citation Index (ESCI), Academic Search Premier, Directory of Open Access Journals
  • Page Numbers: pp.237-243
  • Keywords: Formal methods, theorem proving, higher-order logic, HOL theorem prover, HOL4
  • Yıldız Technical University Affiliated: Yes

Abstract

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.