INTRODUCTION TO HOL4 THEOREM PROVER

Aksoy K., Tahar S., ZEREN Y.

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

  • Yayın Türü: Makale / Tam Makale
  • Cilt numarası: 10 Sayı: 2
  • Basım Tarihi: 2019
  • Dergi Adı: SIGMA JOURNAL OF ENGINEERING AND NATURAL SCIENCES-SIGMA MUHENDISLIK VE FEN BILIMLERI DERGISI
  • Derginin Tarandığı İndeksler: Emerging Sources Citation Index (ESCI), Academic Search Premier, Directory of Open Access Journals
  • Sayfa Sayıları: ss.237-243
  • Anahtar Kelimeler: Formal methods, theorem proving, higher-order logic, HOL theorem prover, HOL4
  • Yıldız Teknik Üniversitesi Adresli: Evet

Özet

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.