A Brief Overview of HOL4

The HOL4 proof assistant supports specification and proof in classical higher order logic. It is the latest in a long line of similar systems. In this short overview, we give an outline of the HOL4 system and how it may be applied in formal verification.

• Type: Conference
• Year: 2008
• Where: TPHOL
• Authors: Konrad Slind, Michael Norrish
• Keywords: Artificial Intelligence, Assistant Supports Specification, Long Line, Similar Systems, TPHOL 2008