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

in
   

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 (w. i. p.).
  • Go/Igo/Baduk/Weiqi (w. i. p.).
  • ISO 8601 and calendar algorithms (w. i. p).

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 01 Oct 2017 07:41:42 PM EEST
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