HOL theorem-proving system

I Use This!

Activity Not Available

Analyzed 3 months ago. based on code collected 3 months ago.

Project Summary

Higher Order Logic (HOL) is a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems. An Oracle mechanism gives access to external programs such as SAT and BDD engines. HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution, and property checking.

In a Nutshell, HOL theorem-proving system...

...
has had 5,416 commits made by 23 contributors
representing 57,061 lines of code
...
is mostly written in Postscript
with a very well-commented source code
...
has a well established, mature codebase
maintained by nobody
with stable Y-O-Y commits
...
took an estimated 14 years of effort (COCOMO model)
starting with its first commit in April, 1999
ending with its most recent commit almost 18 years ago

Quick Reference

Homepage

(2 Locations)

Become the first manager for HOL theorem-proving system

Project Security

Vulnerabilities per Version ( last 10 releases )

There are no reported vulnerabilities

Project Vulnerability Report

Security Confidence Index

Poor security track-record

Favorable security track-record

Vulnerability Exposure Index

Many reported vulnerabilities

Few reported vulnerabilities

About Project Vulnerability Report

Did You Know...

...
use of OSS increased in 65% of companies in 2016
...
you can subscribe to e-mail newsletters to receive update from the Open Hub blog
...
in 2016, 47% of companies did not have formal process in place to track OS code
...
search using multiple tags to find exactly what you need