mainFormalization of mathematics in higher order logic (HOL4 proof assistant) - Summary

Show feedback again
Membership Info
Project Admin:
1 active member

Group identification
Id: #257
System Name: hol-proofs
Name: Formalization of mathematics in higher order logic (HOL4 proof assistant)
Group Type: Software

Search in this Group


Free Software

This is an archive of formalization of pure and applied mathematics in higher order logic (using the HOL4 proof assistant). To download, run “hg clone” in the command line (requires Mercurial). Alternatively visit the repository URL with a web browser.

Current developments:

  • Proof tactics (includes several completed tactics; occasionally more are added).
  • Trivial but necessary lemmas of set theory (expanded as required for the other developments).
  • Partial functions (complete).
  • Topology (in development).
  • Go/Igo/Baduk/Weiqi (in development).
  • ISO 8601 (Gregorian calendar) and algorithms for computation with dates (in development).

This work is licensed under the GNU General Public License version 3 or later, plus an exception to allow redistribution without the license text. The license header is even more concise than the license of Expat (so called “MIT license”). The reader is encouraged to use this license for his own projects instead of a pushover (non-copyleft) license.

Keywords: HOL4; proofs higher order logic; formalization of mathematics; mechanization of mathematics; computer-verified proofs; verified programming.

Registration Date: Sun Oct 1 16:41:42 2017
License: GNU General Public License V3 or later
Development Status: 0 - Undefined


Quick Overview

Show feedback again

Back to the top

Powered by Savane 3.1-cleanup+gray