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 http://hg.gnu.org.ua/hgweb/hol-proofs” 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