HOL.md

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

Name:

HOL

Application domain/field:

Interactive theorem proving Theorem proving Proof assistant Higher-order logic

Type of tool (e.g. model checker, test generator):

Proof assistant

Expected input thing:

Script file

Expected input format:

.sml and .sig files

Expected output:

?

Internals (tools used, frameworks, techniques, paradigms, ...):

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

URIs (github, websites, etc.):

Project page: https://hol-theorem-prover.org/ Repository: https://github.com/HOL-Theorem-Prover/HOL Guidebook/manual: https://hol-theorem-prover.org/guidebook/

Last commit date:

02 Dec 2022 (default branch) 02 Dec 2022 (last activity)

Last publication date:

List of related papers:

Related tools (tools mentioned or compared to in the paper):

Meta

:: PV6 :: interactive theorem prover :: Source :: https://doi.org/10.1145/3550355.3552426