PV6 ⊧ HOLinteractive theorem prover

Interactive theorem prover/proof assistant for higher-order logic.

Application domain/field

• Interactive theorem proving
• Theorem proving
• Proof assistant
• Higher-order logic

Type of tool

Proof assistant

Expected input

Script file

Format:

.sml and .sig files

Internals

Depending on the complexity of what needs to be proven, the user might need to provide guidance to the proof assistant. It can also prove some things on its own without guidance. It is worth checking out libraries to see whether your problem (or something similar) has already been proven.

Comments

The current version is called HOL4. License: Modified (3-clause) BSD license